1 lemma frees_sort_pushs:
2 āf,K,s. K ā¢ š
+ā¦āsā¦ ā f ā
3 āi,L. ā©*[i] L ā K ā L ā¢ š
+ā¦āsā¦ ā ā«Æ*[i] f.
4 #f #K #s #Hf #i elim i -i
5 [ #L #H lapply (drops_fwd_isid ā¦ H ?) -H //
6 | #i #IH #L #H elim (drops_inv_succ ā¦ H) -H /3 width=1 by frees_sort/
10 lemma frees_gref_pushs:
11 āf,K,l. K ā¢ š
+ā¦Ā§lā¦ ā f ā
12 āi,L. ā©*[i] L ā K ā L ā¢ š
+ā¦Ā§lā¦ ā ā«Æ*[i] f.
13 #f #K #l #Hf #i elim i -i
14 [ #L #H lapply (drops_fwd_isid ā¦ H ?) -H //
15 | #i #IH #L #H elim (drops_inv_succ ā¦ H) -H /3 width=1 by frees_gref/