proposition: Lemma Fiat_Bedrock_Insert: forall (N : nat) (table : FiatWBag N) (tuple : FiatWTuple N) (x : nat), Ensembles.Same_set TuplesF.IndexedElement (TuplesF.insertAt (IndexedEnsemble_TupleToListW table) x (TupleToListW tuple)) (IndexedEnsemble_TupleToListW (Ensembles.Add (FiatWElement N) table {| IndexedEnsembles.elementIndex := x; IndexedEnsembles.indexedElement := tuple |})).
proof: Proof. intros; rewrite Same_set_pointwise. unfold IndexedEnsemble_TupleToListW, TuplesF.insertAt, TuplesF.EnsembleInsert, Ensembles.Add. setoid_rewrite Ensembles_Union_Or. setoid_rewrite Ensembles_Singleton_Eq. unfold RelatedIndexedTupleAndListW. repeat match goal with | _ => cleanup | _ => eassumption | [ H: _ \/ _ |- _ ] => destruct H | [ H: exists _, _ |- _ ] => destruct H | _ => solve [eauto] end. simpl in *; subst. destruct x0; simpl in *; subst; eauto. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.BinNatUtils CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW Fiat.QueryStructure.Specification.Representation.Tuple Bedrock.Memory Coq.Lists.List CertifiedExtraction.Utils