lemma cpr_inv_atom1_drops: ∀h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[h] T2 →
∨∨ T2 = ⓪{I}
| ∃∃K,V,V2,i. ⬇*[i] L ≘ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 &
lemma cpr_inv_atom1_drops: ∀h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[h] T2 →
∨∨ T2 = ⓪{I}
| ∃∃K,V,V2,i. ⬇*[i] L ≘ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 &