PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
rest
refl
rel
1
1
1.
n:
{1...}
2.
m:
n
3.
E:
n
n
Prop
4.
Refl(
n;x,y.x E y)
5.
a:
m
a E a
By:
Unfold `refl` 4
Generated subgoal:
1
4.
a:
n. a E a
5.
a:
m
a E a
About:
a:
n. a E am
a E ann
nPropn;x,y.x E y)m a E aa:n. a E am a E a
