proposition: Lemma ImplementListInsert_neq qsSchema Ridx Ridx' (tup : RawTuple) (or : UnConstrQueryStructure qsSchema) (nr : list (RawTuple)) m : Ridx <> Ridx' -> EnsembleIndexedListEquivalence (GetUnConstrRelation or Ridx) nr -> refine {a | EnsembleIndexedListEquivalence (GetUnConstrRelation (@UpdateUnConstrRelation qsSchema or Ridx' (EnsembleInsert {| elementIndex := m; indexedElement := tup|} (GetUnConstrRelation or Ridx'))) Ridx) a} (ret nr).
proof: Proof. unfold refine; intros; computes_to_inv; subst; computes_to_constructor. unfold GetUnConstrRelation, UpdateUnConstrRelation in *. rewrite ith_replace2_Index_neq; eauto using string_dec. 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