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