def Lean.Meta.Grind.propagateProjEq (parent : Expr) : GoalM Unit

If parent is a projection-application proj_i c, check whether the root of the equivalence class containing c is a constructor-application ctor ... a_i .... If so, internalize the term proj_i (ctor ... a_i ...) and add the equality proj_i (ctor ... a_i ...) = a_i.

Equations

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