-(*
-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.
-*)