{
[A,B:Top].
(rec-case(A)
of
[]
=
>
B
|
a::_
=
>
r.[a
/
r]
~
A
@
B)
}
{
Proof
}
Definitions occuring in Statement
:
append:
as
@
bs
,
uall:
[x:A].
B[x]
,
top:
Top
,
list_ind:
list_ind def
,
cons:
[car
/
cdr]
,
sqequal:
s
~
t
Definitions
:
uall:
[x:A].
B[x]
,
append:
as
@
bs
,
member:
t
T
Lemmas
:
top_wf
\mforall{}[A,B:Top]. (rec-case(A) of [] => B | a::$_{}$ => r.[a / r] \msim{} A @ B)
Date html generated: 2011_08_10-AM-07_52_56
Last ObjectModification: 2011_06_18-AM-08_14_52
Home
Index
[x:A]. B[x], [A,B:Top]. (rec-case(A) of [] => B | a::_ => r.[a / r] ~ A @ B) }[x:A]. B[x], [x:A]. B[x], 
T