proposition: Lemma CompileWordList_new: forall (vlst : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) tenv ext (fnew : GLabelMap.key), vlst ∉ ext -> NotInTelescope vlst tenv -> GLabelMap.MapsTo fnew (Axiomatic QsADTs.WordListADTSpec.New) env -> {{ tenv }} Call vlst fnew (nil) {{ [[(NTSome vlst (H := WrapInstance (H := QS_WrapWordList))) ->> @nil W as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t); facade_eauto. change (ADT (QsADTs.WordList [])) with (wrap (FacadeWrapper := WrapInstance (H := @QS_WrapWordList)) []). facade_eauto. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core