PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: list quo choice 2 1 1 1 1 1 1 1
1. q:
2. 0 < q
3. E: q*q*Prop
4. (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y))
5. q = 0
6. x: q*
7. y: q*

(nil E nil) nil = nil q*
By:
Analyze 4
THEN
Unfold `equiv_rel` 4
Generated subgoal:

14. Refl(q*;x,y.x E y) & Sym x,y:q*. x E y & Trans x,y:q*. x E y
5. x,y:q*. Dec(x E y)
6. q = 0
7. x: q*
8. y: q*
(nil E nil) nil = nil q*

About:
nilequallistnatural_numberless_than
functionpropandallint