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.