proposition: Lemma fob_fidentity : forall a x, ob a x -> fob (fidentity a) x = x.
proof: Proof. ir. uf fidentity. uf fob. uf fmor. rww Umorphism.source_identity. rww Umorphism.ev_identity. rw source_id. tv. am. change (is_mor a (id a x)). assert (mor a (id a x)). cw. lu. Qed.
imports: Arith category