gistfile1.txt

visit_unification: r=?3 B A p
 s=B

solution: ?2=fun(B : Type) => fun(A : Type) => fun(p : Prod A B) => A

solution: ?3=fun(B : Type) => fun(A : Type) => fun(p : Prod A B) => B

t: fun(B : Type) => fun(A : Type) => fun(p : Prod A B) => B B A p
 u: B

t: forall (B : Type) (A : Type) (p : Prod A B), B
 u: forall {{B : Type}} {{A : Type}} (p : Prod A B), B

t: Type
 u: Type

t: forall (A : Type) (p : Prod A B), B
 u: forall {{A : Type}} (p : Prod A B), B

t: Type
 u: Type

t: forall (p : Prod A B), B
 u: forall (p : Prod A B), B

fun(B : Type) => fun(A : Type) => fun(p : Prod A B) => A

fun(B : Type) => fun(A : Type) => fun(p : Prod A B) => B