fact: Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) : f == g -> f = g := (@apD10 A P f g)^^-1.
imports: Unicode.Utf8 Coq.Program.Tactics Setoid Relations Equations.Type.All CRelationClasses CMorphisms