def Duper.mkElimDupLitProof (refs : Array (Nat × 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.elimDupLit : MSimpRule

Remove duplicate literals

Equations

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