PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quo of quo 1 2 2 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. 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. x3: T
10. x4: T
11. x3 R x4
12. x2: x,y:T//(x R y)
13. x3 Q x2

x3 = x2 x,y:T//(x Q y)
By: QuotD 12
Generated subgoal:

112. x5: T
13. x6: T
14. x5 R x6
15. x3 Q x5
x3 = x6 x,y:T//(x Q y)

About:
equalquotientuniversefunctionproplambda