proposition: Lemma SubsetIntersectFilter_init : forall { A : Set } (hn : list (A -> Prop)) (init : A -> Prop) (filter : list bool) (x : A), SubsetIntersectFilter hn init filter x -> init x.
proof: Proof. induction hn. - intros. destruct filter; exact H. - intros. destruct filter. exact H. simpl in H. destruct b; apply (IHhn init filter), H. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile