∀ (motive : Std.Tactic.BVDecide.BVLogicalExpr → Sort u_1) (var : Std.Tactic.BVDecide.BVPred)
  (h_1 : (var : Std.Tactic.BVDecide.BVPred) → motive (Std.Tactic.BVDecide.BoolExpr.literal var))
  (h_2 : (val : Bool) → motive (Std.Tactic.BVDecide.BoolExpr.const val))
  (h_3 : (expr : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive expr.not)
  (h_4 : (discr lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive (discr.ite lhs rhs))
  (h_5 :
    (g : Std.Tactic.BVDecide.Gate) →
      (lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) →
        motive (Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs)),
  (match Std.Tactic.BVDecide.BoolExpr.literal var with
    | Std.Tactic.BVDecide.BoolExpr.literal var => h_1 var
    | Std.Tactic.BVDecide.BoolExpr.const val => h_2 val
    | expr.not => h_3 expr
    | discr.ite lhs rhs => h_4 discr lhs rhs
    | Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs => h_5 g lhs rhs) =
    h_1 var