def Lean.Meta.Grind.propagateCtor (a b : Lean.Expr) : Lean.Meta.Grind.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.