PrintForm Definitions languages Sections AutomataTheory Doc

At: lang prod sing 1 1 2 2 2

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

null(l[||l||..||l||])

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

Generated subgoal:

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


About:
assertuniversefunctionlistpropapplyequalnil