proposition: Lemma included_comp : included (Compact Hab) (Dom (G[o]F)).
proof: Proof. intros x H. simpl in |- *. exists (Hf x H). apply Hg. apply maps_lemma' with G a b Hab; assumption. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries