Nuprl - Pf list iso inversion

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

T:Type. Discrete{T} (eq1,eq2:{T}, L,M:T List. eq1 = eq2 L(~eq1)M M(~eq2)L)

By: Analyze 0 THEN Analyze 0 THEN Analyze 0 THEN Equivalence -1 THEN Analyze 0 THEN Equivalence -1 THEN UnivCD

Generated subgoal:

1 1. T: Type
2. Discrete{T}
3. eq1: {T}
4. eq1 TT
5. x:T. eq1(x,x)
6. x,y:T. eq1(x,y) eq1(y,x)
7. x,y,z:T. eq1(x,y) eq1(y,z) eq1(x,z)
8. eq2: {T}
9. eq2 TT
10. x:T. eq2(x,x)
11. x,y:T. eq2(x,y) eq2(y,x)
12. x,y,z:T. eq2(x,y) eq2(y,z) eq2(x,z)
13. L: T List
14. M: T List
15. eq1 = eq2 {T}
16. L(~eq1)M
M(~eq2)L

About:

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