∀ (motive : Std.Tactic.BVDecide.Gate → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.Gate.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.Gate.xor) (h_3 : Unit → motive Std.Tactic.BVDecide.Gate.beq)
  (h_4 : Unit → motive Std.Tactic.BVDecide.Gate.or),
  (match Std.Tactic.BVDecide.Gate.and with
    | Std.Tactic.BVDecide.Gate.and => h_1 ()
    | Std.Tactic.BVDecide.Gate.xor => h_2 ()
    | Std.Tactic.BVDecide.Gate.beq => h_3 ()
    | Std.Tactic.BVDecide.Gate.or => h_4 ()) =
    h_1 ()