def Duper.mkBetaEtaReductionProof (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.betaEtaReduction : MSimpRule

Exhaustively apply beta, eta, and zeta reduction to every subterm in the clause

Equations

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