PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
hd
mem
T:Type, L:T*. ||L||
1
mem_f(T;hd(L);L)
By:
Analyze 0
THEN
Analyze 0
THEN
ListInd 2
THEN
Reduce 0
Generated subgoal:
1
1.
T:
Type
2.
L:
T*
3.
u:
T
4.
v:
T*
5.
||v||
1
mem_f(T;hd(v);v)
6.
||v||+1
1
u = u
mem_f(T;u;v)
About:
1 
mem_f(T;hd(v);v)1
u = u 
mem_f(T;u;v) 
T:Type, L:T*. ||L||1 mem_f(T;hd(L);L)1 mem_f(T;hd(v);v)1 u = u mem_f(T;u;v)
