At: mn 232111 1. n: {1...} 2. A: Type 3. L: LangOver(A) 4. L A*Prop 5. R: A*A*Prop 6. Fin(A) 7. EquivRel x,y:A*. x R y 8. n ~ (x,y:A*//(x R y)) 9. x,y,z:A*. (x R y) ((z @ x) R (z @ y)) 10. g: (x,y:A*//(x R y)) 11. l:A*. L(l) g(l) 12. x: x,y:A*//(x R y) 13. y: x,y:A*//(x R y)
Fin(x,y:A*//(x R y)) By: Witness n Generated subgoal: