proposition: Lemma IsPrefix_iff_Prefix : forall (s s' : list X.t), IsPrefix s s' = true <-> Prefix s s'.
proof: Proof. unfold Prefix; split; revert s'; induction s; intros s' H. - eexists s'; reflexivity. - destruct s'; simpl in H. + discriminate. + destruct (F.eq_dec a t); [subst | discriminate]. unfold IsPrefix in IHs. destruct (IHs s'). destruct (Prefix_dec F.eq_dec s s'); try discriminate; eauto. eexists; subst; eauto. simpl; econstructor; eauto. - simpl; reflexivity. - destruct s'; simpl in *; destruct H. + inversion H. + inversion H; subst; destruct (F.eq_dec a t). destruct (Prefix_dec F.eq_dec s s'); eauto. exfalso; apply n; eexists; eauto. congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListPrefix