PrintForm Definitions relation autom Sections AutomataTheory Doc

At: rest refl rel 1 1 1

1. n: {1...}
2. m: n
3. E: nnProp
4. a:n. a E a
5. a: m

a E a

By: InstHyp [a] 4

Generated subgoals:

None


About:
natural_numberfunctionpropall