theorem Duper.loob_hoist_proof (f : Prop → Prop) (e : Prop) (H : f e) : f True ∨ e = False

theorem Duper.bool_hoist_proof (f : Prop → Prop) (e : Prop) (H : f e) : f False ∨ e = True

def Duper.mkBoolHoistProof (pos : ClausePos) (sgn : Bool) (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def Duper.identBoolHoistAtExpr (e : Lean.Expr) (pos : ClausePos) (c : MClause) : RuleM.RuleM (Option (Array (Clause × RuleM.Proof)))

Equations

• One or more equations did not get rendered due to their size.

def Duper.identBoolHoist : MSimpRule

Equations

• One or more equations did not get rendered due to their size.