Thm* 'a,'b:S.
Thm* all
Thm* ( b:'b. all
Thm* ( b:'b. ( a:'a. all
Thm* ( b:'b. ( a:'a. ( y:'b. all
Thm* ( b:'b. ( a:'a. ( y:'b. ( x:'a. equal
Thm* ( b:'b. ( a:'a. ( y:'b. ( x:'a. (equal(pair(x,y),pair(a,b))
Thm* ( b:'b. ( a:'a. ( y:'b. ( x:'a. ,and(equal(x,a),equal(y,b))))))) | [hpair_eq] |