#J #L #HLK #H destruct /3 width=1 by frees_lref/
]
qed.
-(*
-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.
#I #Y #HYK #H destruct /3 width=1 by frees_lref/
]
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.
-*)
+
(* Advanced inversion lemmas ************************************************)
lemma frees_inv_lref_drops: