proposition: Lemma Fun2_l_id_law : Fid_law FunSET2_l_map.
proof: Proof. unfold Fid_law, FunSET2_l_map, FunSET2_l_mor in |- *; simpl in |- *. unfold Ext, Id_SET in |- *; simpl in |- *. unfold FunSET2_l_mor1 in |- *; simpl in |- *. unfold FunSET2_l_ob in |- *; simpl in |- *; intros dxc f. unfold Id_fun in |- *. apply Trans with (Id (OB_l dxc) o f o FMor G (Id (Ob_r dxc))). apply Ass1. apply Trans with (f o FMor G (Id (Ob_r dxc))). apply Idl. apply Trans with (f o Id (G (Ob_r dxc))). apply Comp_l; apply FId. apply Idr1. Qed.
imports: SET Dual PROD Functor