proposition: Lemma FiniteTables_AbsR_Insert {qs_schema} : forall r_o r_n idx tup, FiniteTables_AbsR r_o r_n -> UnConstrFreshIdx (ith2 r_o idx) (elementIndex tup) -> refine {r_n0 : UnConstrQueryStructure qs_schema | FiniteTables_AbsR (UpdateUnConstrRelation r_o idx (EnsembleInsert tup (GetUnConstrRelation r_o idx))) r_n0} (ret (UpdateUnConstrRelation r_n idx (EnsembleInsert tup (GetUnConstrRelation r_n idx)))).
proof: Proof. intros; refine pick val _; try split; eauto. - destruct H; subst; reflexivity. - destruct H; intros idx'; destruct (fin_eq_dec idx idx'); subst; unfold GetUnConstrRelation, UpdateUnConstrRelation. + rewrite ith_replace2_Index_eq. destruct (H1 idx') as [l ?]; eexists (cons (indexedElement tup) l). eauto using UnIndexedEnsembleListEquivalence_Insert. + rewrite ith_replace2_Index_neq; eauto. Qed.
imports: Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool Coq.Sets.Ensembles Coq.Logic.FunctionalExtensionality Fiat.ADTNotation Fiat.Common Fiat.Common.ilist2 Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure