'a,'b:S.
Thm* equal
Thm* (rep_prod
Thm* ,select
Thm* ,(
rep:hprod('a; 'b)
Thm* ,(
'a
Thm* ,(
'b
Thm* ,(
hbool. and
Thm* ,(
hbool. (all
Thm* ,(
hbool. ((p':hprod('a; 'b). all
Thm* ,(
hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). implies
Thm* ,(
hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). (equal
Thm* ,(
hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). ((rep(p')
Thm* ,(
hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). (,rep(p''))
Thm* ,(
hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). ,equal(p',p''))))
Thm* ,(
hbool. ,all
Thm* ,(
hbool. ,(p:'a 'b hbool. equal
Thm* ,(
hbool. ,(p:'a 'b hbool. (is_pair(p)
Thm* ,(
hbool. ,(p:'a 'b hbool. ,exists
Thm* ,(
hbool. ,(p:'a 'b hbool. ,(p':hprod('a; 'b). equal
Thm* ,(
hbool. ,(p:'a 'b hbool. ,(p':hprod('a; 'b). (p
Thm* ,(
hbool. ,(p:'a 'b hbool. ,(p':hprod('a; 'b). ,rep(p'))))))))'a,'b:S.
Thm* (
p:'a
'b. a:'a. b:'b. (a =
1of(p))
(b = 2of(p)))
Thm* =
Thm* (@
rep:'a'b'a'b
Thm* (@
((p',p'':'a'b. ((rep(p')) = (rep(p'')))
(p' = p''))
Thm* (@
(x:'a'b. ((is_pair(x)) = (
p':'a'b. (x = (rep(p'))))))))