Nuprl Lemma : append-normal-form
∀[A,B:Top]. (rec-case(A) of [] => B | a::_ => r.[a / r] ~ A @ B)
Proof
Definitions occuring in Statement :
append: as @ bs,
list_ind: list_ind,
cons: [a / b],
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions :
cons: [a / b],
append: as @ bs
Lemmas :
top_wf
\mforall{}[A,B:Top]. (rec-case(A) of [] => B | a::$_{}$ => r.[a / r] \msim{} A @ B)
Date html generated:
2015_07_17-AM-09_15_16
Last ObjectModification:
2015_02_02-PM-06_30_45
Home
Index