proposition: Lemma SubsetIntersectFilterOut : forall {A : Set} (hn : list (A -> Prop)) (x : A), (forall filter : list bool, length filter = length hn -> ~SubsetIntersectFilter hn (SubsetUnion hn) filter x) -> Forall (fun h => ~h x) hn.
proof: Proof. induction hn. - intros. apply Forall_nil. - intros. assert (a x -> forall filter : list bool, length filter = length hn -> ~ SubsetIntersectFilter hn (SubsetUnion (a :: hn)) filter x). { intros. intro abs. apply (H (true :: filter)). simpl. apply f_equal. exact H1. split. exact H0. exact abs. } assert (a x -> Forall (fun h => ~h x) hn). { intros. apply IHhn. intros. specialize (H0 H1 filter H2). intro abs. apply H0. apply (SubsetIntersectFilterInc hn (SubsetUnion hn) _ filter x). intros. right. exact H3. exact abs. } assert (~a x). { intro abs. apply (H0 abs (ConstFilter false (length hn))). specialize (H1 abs). apply ConstFilter_length. apply ConstFilter_false. left. exact abs. exact (H1 abs). } clear H0. clear H1. apply Forall_cons. + exact H2. + apply IHhn. intros. intro abs. apply (H (false :: filter)). simpl. apply f_equal, H0. split. 2: exact H2. apply (SubsetIntersectFilterInc hn (SubsetUnion hn) _ filter x). intros. right. exact H1. exact abs. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile