fact: Definition pforall_from_pointed {A : pType} {B : A -> Type} (f : forall x, B x) : pForall A (Build_pFam B (f (point A))) := Build_pForall A (Build_pFam B (f (point A))) f 1%path.
imports: Basics Types Pointed.Core