fact: Definition pmap_compose_ppforall2 {A : pType} {P Q : A -> pType} {g g' : forall (a : A), P a ->* Q a} {f f' : ppforall (a : A), P a} (p : forall a, g a ==* g' a) (q : f ==* f') : pmap_compose_ppforall g f ==* pmap_compose_ppforall g' f'.
imports: Basics Types Pointed.Core