There is one library file in the directory lib_prod with the definition of (non-dependent) cross-product. As well as the basic definitions there are also theorems giving the -rule for pairs and the fact that pairing is extensional.
** Module lib_prod Imports lib_eq_basics $prod : (Type)->(Type)->Type(prod) $pair1 : {A:Type}{B:Type}A->B->prod A B $prod_elim : {A:Type}{B:Type}{C_prod:(prod A B)->Type} ({a:A}{b:B}C_prod (pair1 A B a b))->{z:prod A B}C_prod z [[A:Type][B:Type][C_prod:(prod A B)->Type] [f_pair1:{a:A}{b:B}C_prod (pair1 A B a b)][a:A][b:B] prod_elim A B C_prod f_pair1 (pair1 A B a b) ==> f_pair1 a b] Pair = ... : {A|Type}{B|Type}A->B->prod A B prod_rec = ... : {s|Type}{t|Type}{u|Type}(s->t->u)->(prod s t)->u prod_ind = ... : {s|Type}{t|Type}{P:(prod s t)->Prop}({a:s}{b:t}P (Pair a b))-> {p:prod s t}P p Fst = ... : {s|Type}{t|Type}(prod s t)->s Snd = ... : {s|Type}{t|Type}(prod s t)->t prod_eta = ... : {s|Type}{t|Type}{p:prod s t}Eq p (Pair (Fst p) (Snd p)) prod_ext = ... : {s|Type}{t|Type}{p,q:prod s t}(Eq (Fst p) (Fst q))-> (Eq (Snd p) (Snd q))->Eq p q