( True ) ?A -> ?A
?A ( True ) -> ?A
R ?A ?B -> ( ?A AND ?B ) : Set
( pair ?a ?b ) : ( ?A AND ?B ) -> ( R ?A ) ( ?a : ?A ) ( ?b : ?B )
Nat : Set -> True
zero : Nat -> True
( ?A AND ?B ) : Set -> ( ?A : Set ) ( ?B : Set )
zero : ?n -> Nat
( first ( pair ?a ?b ) ) : ?A -> ( R ?A ( ?b : ?B ) ) ( ?a : ?A )
( Nat ) : Set -> True


Query:
(first (pair zero zero)) : Nat