PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quo of quo 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. EquivRel u,v:x,y:T//(x R y). u Q v

EquivRel x,y:T. x Q y
By: BackThru Thm* R:(TTProp). (EquivRel x,y:T. x R y) (Q:((x,y:T//(x R y))(x,y:T//(x R y))Prop). (EquivRel u,v:x,y:T//(x R y). u Q v) (EquivRel x,y:T. x Q y))
Generated subgoals:

None

About:
universefunctionpropquotient