lemma frees_inv_drops_next: āf1,L1,T1. L1 ā¢ š
*ā¦T1ā¦ ā” f1 ā
āI2,L2,V2,n. ā¬*[n] L1 ā” L2.ā{I2}V2 ā
āg1. ā«Æg1 = ā«±*[n] f1 ā
lemma frees_inv_drops_next: āf1,L1,T1. L1 ā¢ š
*ā¦T1ā¦ ā” f1 ā
āI2,L2,V2,n. ā¬*[n] L1 ā” L2.ā{I2}V2 ā
āg1. ā«Æg1 = ā«±*[n] f1 ā