PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux6 quo 1 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
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

a Q a
By: BackThru 5
Generated subgoals:

None

About:
universefunctionpropquotientallimplies