(* Advanced properties ******************************************************)
-lemma frees_atom_drops:
+lemma frees_atom_drops:
āb,L,i. ā©*[b,šā“iāµ] L ā ā ā
āf. šā¦fā¦ ā L ā¢ š
+ā¦#iā¦ ā ā«Æ*[i]āf.
#b #L elim L -L /2 width=1 by frees_atom/
qed.
lemma frees_pair_drops:
- āf,K,V. K ā¢ š
+ā¦Vā¦ ā f ā
+ āf,K,V. K ā¢ š
+ā¦Vā¦ ā f ā
āi,I,L. ā©*[i] L ā K.ā{I}V ā L ā¢ š
+ā¦#iā¦ ā ā«Æ*[i] āf.
#f #K #V #Hf #i elim i -i
[ #I #L #H lapply (drops_fwd_isid ā¦ H ?) -H /2 width=1 by frees_pair/
#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: