theorem Duper.c1_soundness {p q : Prop} (h : p = q) : p = True ∨ q = False

def Duper.mkC1Proof (i : Nat) (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.

theorem Duper.c2_soundness {p q : Prop} (h : p = q) : p = False ∨ q = True

def Duper.mkC2Proof (i : Nat) (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.clausifyPropEq (given : Clause) (c : MClause) (cNum : Nat) : RuleM.RuleM (Array ClauseStream)

Equations

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