proposition: Lemma Ensemble_List_Equivalence_Insert {A} : forall (a : @IndexedElement A) (Ens : @IndexedEnsemble A), ~ In _ (fun idx => exists a', In _ Ens a' /\ elementIndex a' = elementIndex a) a -> refine {l | UnIndexedEnsembleListEquivalence (EnsembleInsert a Ens) l} (l <- { l | UnIndexedEnsembleListEquivalence Ens l}; ret ((indexedElement a) :: l) ).
proof: Proof. unfold UnIndexedEnsembleListEquivalence, refine, In, EnsembleInsert; intros. computes_to_inv; subst; computes_to_econstructor. destruct_ex; simpl; intuition. exists (a :: x). intuition; subst; simpl; eauto. right; eapply H0; eauto. simpl in *; intuition. right; eapply H0; eauto. econstructor; eauto. unfold not; intros. rewrite in_map_iff in H1; destruct_ex; intuition. apply H0 in H4. eapply H; eexists; eauto. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Common.ilist2 Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Operations.Empty Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Specification.Operations.Update Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements