proposition: Lemma inc_morphism_set : forall r, inc r morphism_set = (inc (source r) obs & inc (target r) obs & inc r (homs (source r) (target r))).
proof: Proof. ir. cp property_hyp. uh H; ee. ap iff_eq; ir. rwi inc_morphism_set1 H7. nin H7. nin H7. ee. rww (H _ _ _ H9). rww (H0 _ _ _ H9). rww (H _ _ _ H9). rww (H0 _ _ _ H9). ee. rw inc_morphism_set1. sh (source r). sh (target r). ee; try am. Qed.
imports: Arith ordinal nat_trans