proposition: Lemma Fun2_r_id_law : Fid_law FunSET2_r_map.
proof: Proof. unfold Fid_law, FunSET2_r_map, FunSET2_r_mor in |- *; simpl in |- *. unfold Ext, Id_SET in |- *; simpl in |- *. unfold FunSET2_r_mor1 in |- *; simpl in |- *. unfold FunSET2_r_ob in |- *; intros dxc f. unfold Id_fun in |- *. apply Trans with (FMor F (Id (OB_l dxc)) o f). apply Idr1. apply Trans with (Id (F (OB_l dxc)) o f). apply Comp_r. apply FId. apply Idl. Qed.
imports: SET Dual PROD Functor