Nuprl - Proof: quotient wf 1

(6steps total) PrintForm Definitions quot 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: quotient wf 1

1. T : Type
2. E : T

Prop
3. EquivRel x,y:T. E(x,y)

x,y:T//E(x,y)

Type

By:	Repeat (Unfolds [`equiv_rel`;`refl`;`sym`;`trans`] 3) THEN Unfold `member` 0 THEN PrimEqCD

Generated subgoals:

1 3. (a:T. E(a,a))
3. & (a,b:T. E(a,b)  E(b,a))
3. & (a,b,c:T. E(a,b)  E(b,c)  E(a,c))
4. x : T
  E(x,x)
1 step

2 3. (a:T. E(a,a))
3. & (a,b:T. E(a,b)  E(b,a))
3. & (a,b,c:T. E(a,b)  E(b,c)  E(a,c))
4. x : T
5. y : T
6. E(x,y)
  E(y,x)
1 step

3 3. (a:T. E(a,a))
3. & (a,b:T. E(a,b)  E(b,a))
3. & (a,b,c:T. E(a,b)  E(b,c)  E(a,c))
4. x : T
5. y : T
6. x1 : T
7. E(x,y)
8. E(y,x1)
  E(x,x1)
2 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(6steps total) PrintForm Definitions quot 1 Sections StandardLIB Doc

1	3. (a:T. E(a,a)) 3. & (a,b:T. E(a,b) E(b,a)) 3. & (a,b,c:T. E(a,b) E(b,c) E(a,c)) 4. x : T E(x,x)	1 step
2	3. (a:T. E(a,a)) 3. & (a,b:T. E(a,b) E(b,a)) 3. & (a,b,c:T. E(a,b) E(b,c) E(a,c)) 4. x : T 5. y : T 6. E(x,y) E(y,x)	1 step
3	3. (a:T. E(a,a)) 3. & (a,b:T. E(a,b) E(b,a)) 3. & (a,b,c:T. E(a,b) E(b,c) E(a,c)) 4. x : T 5. y : T 6. x1 : T 7. E(x,y) 8. E(y,x1) E(x,x1)	2 steps