proposition: Lemma Fun_id_law : Fid_law FunSET_map.
proof: Proof. unfold Fid_law in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold Id_fun in |- *. unfold FunSET_mor1, FunSET_ob in |- *. intros b f; apply Idr1. Qed.
imports: SET Functor Dual