proposition: Lemma EnsembleIndexedListEquivalence_lift_property {heading} {P: @RawTuple heading -> Prop} : forall (sequence: list (@RawTuple heading)) (ensemble: IndexedEnsemble ), EnsembleIndexedListEquivalence ensemble sequence -> ((forall item, List.In item sequence -> P item) <-> (forall item, Ensembles.In _ ensemble item -> P (indexedRawTuple item))).
proof: Proof. intros * equiv; destruct equiv as [? [ l' (is_map & equiv & ?) ] ]; setoid_rewrite equiv. unfold IndexedRawTuple, indexedRawTuple in *. split; intros; firstorder; subst; intuition. eapply H1; eapply in_map_iff; eauto. rewrite in_map_iff in H2; destruct_ex; intuition. subst; eauto. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.SetEq Fiat.Common.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Computation Fiat.ADT Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Operations.Empty Fiat.QueryStructure.Specification.Representation.QueryStructure