PrintForm Definitions languages Sections AutomataTheory Doc

At: lang sing prod 1 2 1 2 1

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

null(l[0..0])

By: RWH (LemmaC Thm* as:T*. null(as) as = nil) 0

Generated subgoal:

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


About:
assertnatural_numberuniversefunctionlist
propapplyequalnil