PrintForm Definitions action sets Sections AutomataTheory Doc

At: el counter wf 1 2

1. n:
2. L: *
3. u:
4. v: *
5. ||n:v||

||n:u.v||

By:
RecCaseSplit `el_counter`
THEN
Inst Thm* a:A, as:A*. ||a.as|| = ||as||+1 [;u;v]


Generated subgoal:

16. u.v = nil
7. n = hd((u.v))
8. ||u.v|| = ||v||+1
||n:v||


About:
memberconsintlist