proposition: Lemma CompileCallFacadeImplementationOfDestructor': forall `{FacadeWrapper av A} {env} fpointer vtmp (adt: Comp A) (tenv: A -> Telescope av), GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationOfDestructor A)) env -> forall vadt ext, vtmp <> vadt -> vtmp ∉ ext -> (forall aadt, adt ↝ aadt -> NotInTelescope vtmp (tenv aadt)) -> vadt ∉ ext -> (forall aadt, adt ↝ aadt -> NotInTelescope vadt (tenv aadt)) -> {{ [[`vadt ~~> adt as aadt]] :: tenv aadt}} (Call vtmp fpointer (vadt :: nil)) {{ [[adt as aadt]] :: tenv aadt }} ∪ {{ ext }} // env.
proof: Proof. intros. apply miniChomp'. intros. rewrite Propagate_ret. eauto using CompileCallFacadeImplementationOfDestructor. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core