proposition: Lemma CompileWordListEmpty_alt: forall {A} {Wrp: FacadeWrapper W A} (vtest vlst : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (tenv: Telescope QsADTs.ADTValue) ext (fempty : GLabelMap.key) (lst : Comp (list A)), vlst <> vtest -> vtest ∉ ext -> Lifted_not_mapsto_adt ext tenv vtest -> GLabelMap.MapsTo fempty (Axiomatic WordListADTSpec.Empty) env -> {{ [[(NTSome (H := WrapSCAList) vlst) ~~> lst as _]] :: tenv }} Call vtest fempty (vlst :: nil) {{ [[(NTSome (H := WrapSCAList) vlst) ~~> lst as ls]] :: [[`vtest ->> (bool2w match ls with | nil => true | _ :: _ => false end) as _]] :: (DropName vtest tenv) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t); facade_eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.CertifiedExtraction.Extraction.Extraction Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Wrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Coq.Program.Program Coq.Lists.List Bedrock.Platform.Facade.examples.QsADTs