PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quo of quo 1 2 2 2 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
6. EquivRel x,y:T. x Q y
7. f: (x,y:T//(x Q y))(u,v:(x,y:T//(x R y))//(u Q v))
8. f = (x.x)
9. g: (u,v:(x,y:T//(x R y))//(u Q v))(x,y:T//(x Q y))
10. g = (x.x)

g o f = Id & f o g = Id
By:
Analyze 0
THEN
RWW "8 10" 0
THEN
Ext
THEN
Reduce 0
Generated subgoals:

111. x: x,y:T//(x Q y)
x = x
211. x: u,v:(x,y:T//(x R y))//(u Q v)
x = x

About:
andequalfunctionquotientuniverseproplambda