lemma frees_sort_pushs:
      ∀f,K,s. K ⊢ 𝐅+⦃⋆s⦄ ≘ f →
      ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃⋆s⦄ ≘ ⫯*[i] f.
#f #K #s #Hf #i elim i -i
[ #L #H lapply (drops_fwd_isid … H ?) -H //
| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_sort/
]
qed.

lemma frees_gref_pushs:
      ∀f,K,l. K ⊢ 𝐅+⦃§l⦄ ≘ f →
      ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃§l⦄ ≘ ⫯*[i] f.
#f #K #l #Hf #i elim i -i
[ #L #H lapply (drops_fwd_isid … H ?) -H //
| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_gref/
]
qed.