-lemma uni_inv_push_dx: ∀f,n. 𝐔❨n❩ ≡ ⫯f → 0 = n ∧ 𝐈𝐝 ≡ f.
-#f * /3 width=5 by eq_inv_pp, conj/
-#n <uni_succ #H elim (eq_inv_np … H) -H //
+lemma uni_inv_push_dx: ∀f,n. 𝐔❨n❩ ≡ ⫯f → 𝟎 = n ∧ 𝐈𝐝 ≡ f.
+#f #n @(nat_ind_succ … n) -n
+[ /3 width=5 by eq_inv_pp, conj/
+| #n #_ <uni_succ #H elim (eq_inv_np … H) -H //
+]