p = true & I = Abbr & c = cT+𝟙𝟘.
/2 width=3 by cpg_inv_bind1_aux/ qed-.
lemma cpg_inv_abbr1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G,L⦄ ⊢ ⓓ{p}V1.T1 ⬈[Rt,c,h] U2 →
∨∨ ∃∃cV,cT,V2,T2. ⦃G,L⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⦃G,L.ⓓV1⦄ ⊢ T1 ⬈[Rt,cT,h] T2 &
U2 = ⓓ{p}V2.T2 & c = ((↕*cV)∨cT)
p = true & I = Abbr & c = cT+𝟙𝟘.
/2 width=3 by cpg_inv_bind1_aux/ qed-.
lemma cpg_inv_abbr1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G,L⦄ ⊢ ⓓ{p}V1.T1 ⬈[Rt,c,h] U2 →
∨∨ ∃∃cV,cT,V2,T2. ⦃G,L⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⦃G,L.ⓓV1⦄ ⊢ T1 ⬈[Rt,cT,h] T2 &
U2 = ⓓ{p}V2.T2 & c = ((↕*cV)∨cT)