(2steps) PrintForm core 3 jlc Sections Support(jlc) Doc

At: pair functionality wrt equal 1
1. T: Type
2. U: Type
3. t1: T
4. t2: T
5. u1: U
6. u2: U
7. t1 = t2
8. u1 = u2

< t1,u1 > = < t2,u2 >
By:
OnHyps [7;8] (i.UnfoldTopAb i)
THEN
MemberEqCD
THEN
Trivial
Generated subgoals:

None

About:
pairproductuniverseequal

(2steps) PrintForm core 3 jlc Sections Support(jlc) Doc