# A general pairing interface param (PROP pax/prop () "") param (PRED pax/pred (PROP) "") param (A pax/basetype (PROP PRED) "A.") param (B pax/basetype (PROP PRED) "B.") param (AxB pax/basetype (PROP PRED) "AxB.") var (val a b a' b') term (val (pair val val)) stmt (pair-ty () () (-> (/\ (: a (A.T)) (: b (B.T))) (: (pair a b) (AxB.T)))) stmt (ax-pair () () (-> (/\ (/\ (: a (A.T)) (: b (B.T))) (/\ (: a' (A.T)) (: b' (B.T)))) (<-> (/\ (= (A.T) a a') (= (B.T) b b')) (= (AxB.T) (pair a b) (pair a' b')))))