'a,'b:S, x:('a
'b). <1of(x),2of(x)> = x'a,'b:S. all(
x:hprod('a; 'b). equal(pair(fst(x),snd(x)),x))| Theorem | Name |
| 'a,'b:S, x:('a'b). <1of(x),2of(x)> = x | [pair_wd] |
| cites the following: | |
| 'a,'b:S. all(x:hprod('a; 'b). equal(pair(fst(x),snd(x)),x)) | [hpair_wd] |