proposition: Lemma get_update_unconstr_neq : forall (db_schema : RawQueryStructureSchema) (qs : UnConstrQueryStructure db_schema) (index1 index2 : _) ens, index1 <> index2 -> GetUnConstrRelation (UpdateUnConstrRelation qs index1 ens) index2 = GetUnConstrRelation qs index2.
proof: Proof. unfold UpdateUnConstrRelation, GetUnConstrRelation; intros; simpl; rewrite ith_replace2_Index_neq; eauto using string_dec. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.Common.StringBound Fiat.Common.ilist2 Fiat.Common.ilist Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Schema Fiat.QueryStructure.Specification.Representation.Relation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema