proposition: Lemma Monic_inj : SET_Monic_law f -> Inj_law f.
proof: Proof. unfold Monic_law in |- *; intros H1; unfold Inj_law in |- *. intros x y H2. generalize (H1 _ (MapConst x) (MapConst y)). intros H3; exact (H3 (fun z : B => H2) (f x)). Qed.
imports: SET CatProperty MapProperty