Nuprl - Pf list iso functionality wrt id list iso list iso

(9steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: list iso functionality wrt id list iso list iso

T:Type, L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L3(~eq2)L4 (L1(~eq3)L3 L2(~eq3)L4)

By: RepeatFor 3 (Analyze 0) THEN RepeatFor 3 (Analyze 0 THEN EquivT -1) THEN UnivCD

Generated subgoal:

1 1. T: Type
2. L1: T List
3. L2: T List
4. eq1: {T}
5. eq1 TT
6. eq2: {T}
7. eq2 TT
8. eq3: {T}
9. eq3 TT
10. L3: T List
11. L4: T List
12. Discrete{T}
13. eq1 = eq2 {T}
14. eq2 = eq3 {T}
15. L1(~eq1)L2
16. L3(~eq2)L4
L1(~eq3)L3 L2(~eq3)L4

About:

(9steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc