proposition: Lemma SubsetUnionLeftDec : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyH : Domain (ProdLFunc hn) (x,y)), (SubsetUnion (map prodint_f hn) x /\ ~Forall (fun fg => ~prodint_f fg x) hn) \/ (Forall (fun fg => ~prodint_f fg x) hn /\ ~SubsetUnion (map prodint_f hn) x).
proof: Proof. induction hn. - intros. right. split. apply Forall_nil. intro abs. exact abs. - intros. destruct xyH. destruct (IHhn x y d0). + left. split. right. apply H. intro abs. inversion abs. destruct H. contradiction. + simpl. destruct d, d. left. split. left. exact p. intro abs. inversion abs. destruct H. contradiction. right. split. apply Forall_cons. exact n. apply H. intro abs. destruct abs. contradiction. destruct H. contradiction. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile