At: incl aux6 quo 1 1 1 3
1. T: Type
2. R: T
TProp
3. EquivRel x,y:T. x R y
4. Q: (x,y:T//(x R y))(x,y:T//(x R y))Prop
5. 
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
By: FwdThru 7 [11;12]
Generated subgoals:None
About:
