proposition: Corollary Iterate_Ensemble_filter_neq {n} : forall (P : Ensemble (Fin.t n)) (Ridx : Fin.t n), (forall idx, idx <> Ridx -> P idx) <-> (@Iterate_Ensemble_BoundedIndex_filter n P (fun idx => if (fin_eq_dec Ridx idx) then false else true)).
proof: Proof. intros. assert (forall a : Fin.t n, (if fin_eq_dec Ridx a then false else true) = true <-> a <> Ridx) as filter_dec' by (intros; find_if_inside; try rewrite e; intuition). split; intros. - eapply Iterate_Ensemble_equiv_filter'' with (filter := fun idx => idx <> Ridx) (filter_dec := {|dec_decides_P := filter_dec' |}); eauto. - eapply Iterate_Ensemble_equiv_filter' with (filter := fun idx => idx <> Ridx) (filter_dec := {|dec_decides_P := filter_dec' |}); unfold dec; eauto using string_dec. 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