def Lean.Meta.Grind.propagateForallProp (parent : Lean.Expr) : Lean.Meta.Grind.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.
• Lean.Meta.Grind.propagateForallProp parent = pure ()