{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.
Require Import Basics Types. Require Import Pointed.Core.