proposition: Lemma CompileEmpty {idx}: forall (vtest vlst : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (tenv: Telescope QsADTs.ADTValue) ext (fpointer : GLabelMap.key) (lst : list (RealElemType idx)), vlst <> vtest -> vtest ∉ ext -> Lifted_MapsTo ext tenv vlst (wrap lst) -> Lifted_not_mapsto_adt ext tenv vtest -> GLabelMap.MapsTo fpointer (Axiomatic Empty) env -> {{ tenv }} Call vtest fpointer (vlst :: nil) {{ [[`vtest ->> (bool2w (Nat.eqb (Datatypes.length lst) 0)) as _]] :: (DropName vtest tenv) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t || PreconditionSet_t || injections). facade_eauto. rewrite add_remove_comm by congruence. rewrite <- add_redundant_cancel by assumption. facade_eauto. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists