PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux6 quo 1 1 1
1. T: Type
2. R: TTProp
3. EquivRel x,y:T. x R y
4. Q: (x,y:T//(x R y))(x,y:T//(x R y))Prop

(a:x,y:T//(x R y). a Q a) & (a,b:x,y:T//(x R y). (a Q b) (b Q a)) & (a,b,c:x,y:T//(x R y). (a Q b) (b Q c) (a Q c)) (a:T. a Q a) & (a,b:T. (a Q b) (b Q a)) & (a,b,c:T. (a Q b) (b Q c) (a Q c))
By: GenRepD
Generated subgoals:

15. a:x,y:T//(x R y). a Q a
6. a,b:x,y:T//(x R y). (a Q b) (b Q a)
7. a,b,c:x,y:T//(x R y). (a Q b) (b Q c) (a Q c)
8. a: T
a Q a
25. a:x,y:T//(x R y). a Q a
6. a,b:x,y:T//(x R y). (a Q b) (b Q a)
7. a,b,c:x,y:T//(x R y). (a Q b) (b Q c) (a Q c)
8. a: T
9. b: T
10. a Q b
b Q a
35. a:x,y:T//(x R y). a Q a
6. a,b:x,y:T//(x R y). (a Q b) (b Q a)
7. a,b,c:x,y:T//(x R y). (a Q b) (b Q c) (a Q c)
8. a: T
9. b: T
10. c: T
11. a Q b
12. b Q c
a Q c

About:
impliesandallquotientuniversefunctionprop