fact: Definition ap10_path_forall {A B : Type} (f g : A -> B) (h : f == g) : ap10 (path_forall f g h) == h := apD10_path_forall f g h.
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall