proposition: Lemma CompileDeallocW: forall {av} (env : Env av) k (compSCA: Comp W) tail tail' ext prog, {{ [[compSCA as kk]]::(tail kk)}} prog {{ [[compSCA as kk]]::(tail' kk) }} ∪ {{ ext }} // env -> {{ [[`k ~~> compSCA as kk]]::(tail kk)}} prog {{ [[compSCA as kk]]::(tail' kk) }} ∪ {{ ext }} // env.
proof: Proof. eauto using CompileDeallocSCA. Qed.
imports: CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics