proposition: Lemma refineEquivUnion {T A} P (P_respectful : forall S1 S2 x, Same_set A S1 S2 -> (P S1 x <-> P S2 x)) (S1 S2 : Ensemble A) : refine { x : T | P (Ensembles.Union A S1 S2) x } (ls1 <- to_list S1; ls2 <- to_list S2; { x : T | P (elements (ls1 ++ ls2)) x }).
proof: Proof. unfold to_list, elements; repeat intro; inversion_by computes_to_inv. constructor. eapply P_respectful; try eassumption. repeat first [ split | progress hnf in * | intro | progress destruct_head_hnf Union | progress destruct_head_hnf and | progress destruct_head_hnf or | progress split_iff | match goal with H : List.In _ (_ ++ _) |- _ => apply in_app_or in H end | apply in_or_app | progress unfold Ensembles.In in * | left; unfold Ensembles.In in *; solve [ eauto ] | right; unfold Ensembles.In in *; solve [ eauto ] ]. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.RelationPairs Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTNotation Fiat.ADTRefinement.GeneralRefinements Fiat.Computation Fiat.Common Fiat.Common.Ensembles Fiat.Common.Ensembles.Tactics Fiat.ComputationalEnsembles Fiat.FiniteSetADTs.FiniteSetADTMethodLaws Fiat.FiniteSetADTs.FiniteSetADT