(* 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/