def Lean.Meta.Match.simpH? (h : Expr) (numEqs : Nat) : MetaM (Option Expr)

Auxiliary method for simplifying equational theorem hypotheses.

Recall that each equation contains additional hypotheses to ensure the associated case was not taken by previous cases. We have one hypothesis for each previous case.

Equations

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