fact: Definition functor2_pforall_right {A : pType} {B C : pFam A} {g g' : forall (a : A), B a -> C a} {g₀ : g (point A) (dpoint B) = dpoint C} {g₀' : g' (point A) (dpoint B) = dpoint C} {f f' : pForall A B} (p : forall a, g a == g' a) (q : f ==* f') (r : p (point A) (dpoint B) @ g₀' = g₀) : functor_pforall_right g g₀ f ==* functor_pforall_right g' g₀' f'.
imports: Basics Types Pointed.Core