PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux5 quo 1 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 E y

By:
Unfolds [`equiv_rel`] 3
THEN
Unfold `refl` 3
THEN
Analyze 3


Generated subgoal:

13. a:T. a E a
4. Sym x,y:T. x E y & Trans x,y:T. x E y
5. x: T
6. y: T
7. x = y
x E y


About:
universefunctionpropequal