proposition: Lemma CompileEmpty_spec {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 -> NotInTelescope vtest tenv -> StringMap.MapsTo vlst (wrap lst) ext -> GLabelMap.MapsTo fpointer (Axiomatic Empty) env -> {{ tenv }} Call vtest fpointer (vlst :: nil) {{ [[`vtest ->> (bool2w (Nat.eqb (Datatypes.length (rev lst)) 0)) as _]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. setoid_rewrite rev_length. apply generalized @CompileEmpty; repeat (compile_do_side_conditions || Lifted_t). Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists