proposition: Lemma CompileNew {idx} : forall vret fpointer (env: Env ADTValue) ext tenv, GLabelMap.find fpointer env = Some (Axiomatic New) -> vret ∉ ext -> Lifted_not_mapsto_adt ext tenv vret -> {{ tenv }} Call vret fpointer nil {{ [[ `vret ->> @nil (RealElemType idx) as _ ]] :: DropName vret tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t). change (ADT (ListConstructor [])) with (wrap (FacadeWrapper := WrapInstance (H := @WrapADTList idx)) []). facade_eauto. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists