∀ {α : Type} (a : Std.Tactic.BVDecide.Gate) (a_1 a_2 : Std.Tactic.BVDecide.BoolExpr α) (a_3 : Std.Tactic.BVDecide.Gate)
  (a_4 a_5 : Std.Tactic.BVDecide.BoolExpr α),
  (Std.Tactic.BVDecide.BoolExpr.gate a a_1 a_2 = Std.Tactic.BVDecide.BoolExpr.gate a_3 a_4 a_5) =
    (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)