PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
incl
aux5
quo
1
1
1.
T:
Type
2.
E:
T
T
Prop
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:
1
3.
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:
a:T. a E a
x E y
TProp x E ya:T. a E a x E y
