proposition: Lemma CompileCallFacadeImplementationOfDestructor: forall `{FacadeWrapper av A} {env} fpointer vtmp (adt: A) (tenv: Telescope av), GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationOfDestructor A)) env -> forall vadt ext, vtmp <> vadt -> vtmp ∉ ext -> NotInTelescope vtmp tenv -> vadt ∉ ext -> NotInTelescope vadt tenv -> {{ [[ `vadt ->> adt as _]] :: tenv }} (Call vtmp fpointer (vadt :: nil)) {{ tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat match goal with | _ => SameValues_Facade_t_step | _ => facade_cleanup_call | _ => PreconditionSet_t end; facade_eauto. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core