+(* Basic properties *********************************************************)
+
+lemma nexts_O: ∀f. f = ↑*[𝟎] f.
+// qed.
+
+lemma nexts_S: ∀f,n. ↑↑*[n] f = ↑*[↑n] f.
+#f #n @(niter_succ … next)
+qed.
+
+lemma nexts_eq_repl: ∀n. eq_repl (λf1,f2. ↑*[n] f1 ≡ ↑*[n] f2).
+#n @(nat_ind_succ … n) -n /3 width=5 by eq_next/
+qed.
+
+(* Advanced properties ******************************************************)
+
+lemma nexts_swap: ∀f,n. ↑↑*[n] f = ↑*[n] ↑f.
+#f #n @(niter_appl … next)
+qed.
+
+lemma nexts_xn: ∀n,f. ↑*[n] ↑f = ↑*[↑n] f.
+// qed.
+