PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux6 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

EquivRel x,y:T. x Q y
By:
MoveToConcl 5
THEN
Unfold `equiv_rel` 0
Generated subgoal:

1 Refl(x,y:T//(x R y);u,v.u Q v) & Sym u,v:x,y:T//(x R y). u Q v & Trans u,v:x,y:T//(x R y). u Q v Refl(T;x,y.x Q y) & Sym x,y:T. x Q y & Trans x,y:T. x Q y

About:
universefunctionpropquotientimpliesand