proposition: Lemma inc_one : forall x, inc x (R 1) = (x = R 0).
proof: Proof. ir. rw nat_succ_tack_on. ap iff_eq; ir. rwi tack_on_inc H. nin H. rwi zero_emptyset H. nin H. elim x0. am. rw tack_on_inc. ap or_intror; am. Qed.
imports: Arith ordinal nat_trans