pair-beta : A
pair-beta = (fst (the (prod A B) (pair a b)))
pair-beta = (the A a)