#n elim n -n /3 width=5 by eq_push/
qed.
-(* Advancedd properties *****************************************************)
+(* Advanced properties ******************************************************)
lemma pushs_xn: ∀n,f. ↑*[n] ↑f = ↑*[⫯n] f.
#n elim n -n //