Entry	Value
Package Name	pair-def
Count	4
Theorems	FST : !a b. FST (a,b) = a PAIR_EQ : !a b a' b'. a,b = a',b' <=> a = a' /\ b = b' PAIR_SURJECTIVE : !x. ?a b. x = a,b SND : !a b. SND (a,b) = b

Back to main package page