-theorem cpcs_aaa_mono (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 →
- ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
+(* Note: lemma 1500 *)
+theorem cpcs_aaa_mono (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ⬌*[h] T2 →
+ ∀A1. ❪G,L❫ ⊢ T1 ⁝ A1 → ∀A2. ❪G,L❫ ⊢ T2 ⁝ A2 →