PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux5 quo 1

1. T: Type
2. E: TTProp
3. EquivRel x,y:T. x E y
4. x: T
5. y: T
6. x = y

x = y u,v:T//(u E v)

By: Analyze

Generated subgoal:

1 x E y


About:
equalquotientuniversefunctionprop