proposition: Lemma FullyFaithful `(F : C ⟶ D) `{@Full _ _ F} `{@Faithful _ _ F} : ∀ x y, F x ≅ F y → x ≅ y.
proof: Proof. intros. construct. + apply prefmap, X. + apply prefmap, X. + abstract (simpl; rewrite <- prefmap_comp; destruct H; rewrite iso_to_from; apply prefmap_id). + abstract (simpl; rewrite <- prefmap_comp; destruct H; rewrite iso_from_to; apply prefmap_id). Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Equations.Prop.Logic