proposition: Lemma UnIndexedEnsembleListEquivalence_app {A} : forall (P Q : IndexedEnsemble) (l l' : list A), Disjoint _ (fun idx => exists tup, In _ P {| elementIndex := idx; indexedElement := tup |}) (fun idx => exists tup, In _ Q {| elementIndex := idx; indexedElement := tup |}) -> UnIndexedEnsembleListEquivalence P l -> UnIndexedEnsembleListEquivalence Q l' -> UnIndexedEnsembleListEquivalence (Union _ P Q) (l ++ l').
proof: Proof. unfold UnIndexedEnsembleListEquivalence; intros. destruct_ex; intuition. eexists (x0 ++ x)%list; intuition; eauto. - rewrite map_app; congruence. - apply in_or_app. setoid_rewrite <- H1; setoid_rewrite <- H3; destruct H4; intuition. - apply in_app_or in H4. setoid_rewrite <- H1 in H4; setoid_rewrite <- H3 in H4. intuition. - rewrite map_app; apply NoDup_app_in_iff; intuition. apply in_map_iff in H4; apply in_map_iff in H7; destruct_ex; intuition; subst. apply H1 in H10; apply H3 in H9. inversion H; subst. eapply (H0 (elementIndex x2)). destruct x3; destruct x2; subst; simpl in *. econstructor; unfold In. eexists; eauto. rewrite H4; eexists; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.SumType Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Bedrock.Word Bedrock.Memory