PrintForm Definitions languages Sections AutomataTheory Doc

At: lang sing prod 1 2 1 2 1 1

1. Alph: Type
2. L: Alph*Prop
3. l: Alph*
4. L(l)

(l[0..0]) = nil

By: Assert (||l[0..0]|| = 0)

Generated subgoals:

1 ||l[0..0]|| = 0
25. ||l[0..0]|| = 0
(l[0..0]) = nil


About:
equallistnatural_numbernilint
universefunctionpropapply