proposition: Lemma CompileNew_helper : forall vret vsize fpointer (env: Env ADTValue) ext tenv N, GLabelMap.find fpointer env = Some (Axiomatic New) -> Lifted_MapsTo ext tenv vsize (wrap (Word.natToWord 32 N)) -> Lifted_not_mapsto_adt ext (tenv: Telescope ADTValue) vret -> vret ∉ ext -> ~ Word.wlt (Word.natToWord 32 N) (Word.natToWord 32 2) -> {{ tenv }} Call vret fpointer (vsize :: nil) {{ [[ `vret ->> TreeConstructor N Empty as _ ]] :: DropName vret tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t). facade_eauto. facade_eauto. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core