proposition: Lemma ImplementListInsert_eq qsSchema Ridx (tup : RawTuple) (or : UnConstrQueryStructure qsSchema) (nr : list (RawTuple)) (bound : nat) : EnsembleIndexedListEquivalence (GetUnConstrRelation or Ridx) nr -> (UnConstrFreshIdx (GetUnConstrRelation or Ridx) bound) -> refine {a | EnsembleIndexedListEquivalence (GetUnConstrRelation (@UpdateUnConstrRelation qsSchema or Ridx (EnsembleInsert {| elementIndex := bound; indexedElement := tup|} (GetUnConstrRelation or Ridx))) Ridx) a} (ret (tup :: nr)).
proof: Proof. unfold refine; intros; computes_to_inv; subst; computes_to_constructor. unfold GetUnConstrRelation, UpdateUnConstrRelation in *. rewrite ith_replace2_Index_eq. unfold EnsembleInsert, In, EnsembleIndexedListEquivalence, UnConstrFreshIdx in *; intuition. exists (S bound); unfold In in *; destruct_ex; subst; simpl. intros; intuition; subst. simpl. omega. destruct H2 as [l' [l'_eq [equiv_l' NoDup_l'] ] ]. econstructor 1 with ({| elementIndex := bound; indexedElement := tup|} :: l'); split; eauto. simpl; subst; reflexivity. unfold EnsembleListEquivalence in *; intuition. unfold In in *; subst; intuition. subst; simpl; eauto. simpl; right; eapply equiv_l'; eauto. simpl in *; unfold In; intuition. eapply equiv_l' in H2; eauto. simpl; econstructor; eauto. unfold not; intros. rewrite in_map_iff in H; destruct_ex; intuition. apply equiv_l' in H3; apply H0 in H3. simpl in *; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Bool.Bool Fiat.Common.ilist2 Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.ADTRefinement.BuildADTRefinements Fiat.Common.DecideableEnsembles Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.QueryStructureRefinements Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements