proposition: Lemma CompileExtendLifetime: forall {av A} {env ext} (k: NameTag av A) comp tenv tenv' prog dealloc, {{ [[k ~~> comp as kk]] :: tenv kk }} prog {{ [[k ~~> comp as kk]] :: tenv' kk }} ∪ {{ext}} // env -> {{ [[k ~~> comp as kk]] :: tenv' kk }} dealloc {{ [[comp as kk]] :: tenv' kk }} ∪ {{ext}} // env -> {{ [[k ~~> comp as kk]] :: tenv kk }} (Seq prog dealloc) {{ [[comp as kk]] :: tenv' kk }} ∪ {{ext}} // env.
proof: Proof. repeat hoare. Qed.
imports: CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics