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 ā