PrintForm Definitions languages Sections AutomataTheory Doc

At: lang prod sing 1 1 2 2 1

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

L(l[0..||l||])

By: RWH (LemmaC Thm* as:T*. (as[0..||as||]) = as) 0

Generated subgoals:

None


About:
applynatural_numberuniversefunctionlistprop