IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
equiv rel functionality wrt iff
1
1
1
1
1
1
1
1. T : Type
2. T' : Type
3. E : T
T
Prop
4. E' : T'
T'
Prop
5. T = T'
6.
x,y:T. E(x,y) 
E'(x,y)
7.
a:Prop. a 
a
8. (Sym A,B:Prop. A 
B) & (Trans A,B:Prop. A 
B)
(
a:T'. E'(a,a))
& (
a,b:T'. E'(a,b) 
E'(b,a))
& (
a,b,c:T'. E'(a,b) 
E'(b,c) 
E'(a,c))

(
a:T'. E'(a,a))
& (
a,b:T'. E'(a,b) 
E'(b,a))
& (
a,b,c:T'. E'(a,b) 
E'(b,c) 
E'(a,c))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html