proposition: Lemma nat_succ_tack_on : forall (i:nat), R (S i) = tack_on (R i) (R i).
proof: Proof. ir. ap extensionality; uhg; ir. rwi nat_realization_S H. rw tack_on_inc. am. rw nat_realization_S. rwi tack_on_inc H. am. Qed.
imports: Arith ordinal nat_trans