-(*
-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_lref_pushs: ∀f,K,j. K ⊢ 𝐅*⦃#j⦄ ≘ f →
- ∀i,L. ⬇*[i] L ≘ K → L ⊢ 𝐅*⦃#(i+j)⦄ ≘ ⫯*[i] f.
+
+lemma frees_lref_pushs:
+ ∀f,K,j. K ⊢ 𝐅+⦃#j⦄ ≘ f →
+ ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃#(i+j)⦄ ≘ ⫯*[i] f.