def Duper.mkElimResolvedLitProof (refs : List (Option 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.elimResolvedLit : MSimpRule

Eliminate resolved literals (i.e. literals of the form t ≠ t) (Deletion of Resolved Literals: (DR))

Equations

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