proposition: Lemma refine_decides_Equiv_Ensemble {n} : forall (P P' : Ensemble (Fin.t n)) (equiv_P'_P : (forall idx, P idx) <-> (forall idx', P' idx')), refine {b | decides b (forall idx, P idx)} {b | decides b (forall idx, P' idx)}.
proof: Proof. intros * equiv_P'_P v Comp_v. computes_to_inv; computes_to_constructor; destruct v; simpl in *. intros; eapply equiv_P'_P; eauto. unfold not; intros; eapply Comp_v; eapply equiv_P'_P; eauto. Qed.
imports: Coq.Lists.List Coq.Arith.Compare_dec Coq.Arith.Arith Coq.Bool.Bool Coq.Strings.String Coq.Sets.Ensembles Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.Common.IterateBoundedIndex Fiat.Common.List.ListFacts Fiat.Common.LogicFacts Fiat.Common.DecideableEnsembles Fiat.Common.BoundedLookup Fiat.Common.IterateBoundedIndex Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.ApplyMonad Fiat.Computation.SetoidMorphisms Fiat.Computation.Refinements.General Fiat.Computation.Refinements.Tactics