proposition: Lemma Comp_Functor_id_law : Fid_law Comp_FMap.
proof: Proof. unfold Fid_law, Comp_FOb, Comp_FMap, Comp_FMor in |- *. simpl in |- *; intro a. apply Trans with (FMor H (Id (G a))). apply FPres; apply FId. apply FId. Qed.
imports: Setoid_dup1 Hom_Equality