def Lean.Meta.Grind.propagateCtor (a b : Expr) : GoalM Unit

Given constructors a and b, propagate equalities if they are the same, and close goal if they are different.

Equations

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