PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux6 quo 1 1 1 2
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
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. a Q b

b Q a
By: BackThru 6
Generated subgoals:

None

About:
universefunctionpropquotientallimplies