proposition: Lemma CompileDeallocSCA: forall {av} {A} (Wrp: FacadeWrapper (Value av) A) (env : Env av) k (compSCA: Comp A) tail tail' ext prog, (forall a, is_adt (wrap a) = false) -> {{ [[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. SameValues_Facade_t; learn (SameValues_Dealloc_SCA _ _ _ _ _ _ H H1); SameValues_Facade_t. Qed.
imports: CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics