IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l before transitivity12 1. T : Type
2. l : T List
3. x : T 4. y : T 5. z : T 6. no_repeats(T;l)
7. [x; y] l 8. [y; z] l [x; y; z] l
By:
Inst
Thm*L1,L2,L:T List, x:T.
Thm* no_repeats(T;L) L1 @ [x] L [x / L2] LL1 @ [x / L2] L [T;[x];[z];l;y]
THEN
All Reduce
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html