proposition: Lemma inc_two : forall x, inc x (R 2) = ((x = R 0) \/ (x = R 1)).
proof: Proof. ir. rw two_tack_on. ap iff_eq; ir. rwi tack_on_inc H. nin H. rwi inc_one H. ap or_introl; am. ap or_intror; am. rw tack_on_inc. nin H. ap or_introl. rw inc_one. am. ap or_intror; am. Qed.
imports: Arith ordinal nat_trans