proposition: Lemma IsFaithful_comp : Faithful_law F -> Faithful_law G -> Faithful_law (F o_F G).
proof: Proof. intros H1 H2; unfold Faithful_law in |- *; intros a b f g. unfold Comp_Functor, FMor in |- *; simpl in |- *. unfold Comp_FMor in |- *; auto. Qed.
imports: Functor CatProperty