proposition: Lemma CompileDeallocW_discretely : forall {av} (tenv tenv': Telescope av) ext env k (v: Comp W) prog, k ∉ ext -> NotInTelescope k tenv -> {{ [[`k ~~> v as _]] :: tenv }} prog {{ [[`k ~~> v as _]] :: tenv' }} ∪ {{ ext }} // env -> {{ [[`k ~~> v as _]] :: tenv }} prog {{ tenv' }} ∪ {{ ext }} // env.
proof: Proof. SameValues_Facade_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas