PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quo of quo 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

f:((x,y:T//(x Q y))(u,v:(x,y:T//(x R y))//(u Q v))) , g:((u,v:(x,y:T//(x R y))//(u Q v))(x,y:T//(x Q y))). InvFuns(x,y:T//(x Q y); u,v:(x,y:T//(x R y))//(u Q v); f; g)
By: Assert (EquivRel x,y:T. x Q y)
Generated subgoals:

1 EquivRel x,y:T. x Q y
26. EquivRel x,y:T. x Q y
f:((x,y:T//(x Q y))(u,v:(x,y:T//(x R y))//(u Q v))) , g:((u,v:(x,y:T//(x R y))//(u Q v))(x,y:T//(x Q y))). InvFuns(x,y:T//(x Q y); u,v:(x,y:T//(x R y))//(u Q v); f; g)

About:
existsfunctionquotientuniverseprop