proposition: Lemma Y_faithful : Faithful_law0'' FunY.
proof: Proof. unfold Faithful_law0'' in |- *; simpl in |- *. unfold Equal_NT in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; unfold DHom in |- *. unfold NtH_arrow in |- *. unfold FunSET_ob in |- *. intros a b f g H. apply Trans with (g o Id a). apply Trans with (f o Id a). apply Idr. apply H. apply Idr1. Qed.
imports: HomFunctor_NT CatFunct Functor_dup1