proposition: Lemma included_FComp : included R P -> (forall x Hx, (R x) -> Q (F x Hx)) -> included R (Dom (G[o]F)).
proof: Proof. intros HP HQ. simpl in |- *. red in |- *; intros x Hx. exists (HP x Hx). apply HQ. assumption. Qed.
imports: CoRN.algebra.CSetoidFun