-theorem cpc_conf: ∀L,T0,T1,T2. L ⊢ T0 ⬌ T1 → L ⊢ T0 ⬌ T2 →
- ∃∃T. L ⊢ T1 ⬌ T & L ⊢ T2 ⬌ T.
-/3 width=3/ qed.
+theorem cpc_conf: ∀G,L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌ T1 → ⦃G, L⦄ ⊢ T0 ⬌ T2 →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ⬌ T & ⦃G, L⦄ ⊢ T2 ⬌ T.
+/3 width=3 by cpc_sym, ex2_intro/ qed-.