proposition: Lemma Inj_monic : Inj_law f -> SET_Monic_law f.
proof: Proof. unfold Inj_law, SET_Monic_law in |- *; intro H1; unfold Monic_law in |- *. intros C g h H2; simpl in |- *; unfold Ext in |- *; intro x. apply H1; exact (H2 x). Qed.
imports: SET CatProperty MapProperty