proposition: Lemma included_conj : forall P Q R, included P Q -> included P R -> included P (Conj Q R).
proof: Proof. intros. red in |- *; red in X, X0. intros; red in |- *. split. apply X; assumption. apply X0; assumption. Qed.
imports: CoRN.algebra.CSetoidFun