proposition: Lemma ob_from_arrows : forall x, ob from_arrows x = inc x obs.
proof: Proof. ir. ap iff_eq; ir. wrr is_ob_from_arrows. app ob_is_ob. wri is_ob_from_arrows H. app is_ob_ob. ap from_arrows_axioms. Qed.
imports: Arith ordinal nat_trans