partial commit: just the components before "static" ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / conversion / cpc_cpc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
index dcea07a8baa8e85ed6118970b5ced6ec15797f56..092d2a9a753d9dffad0cc61eece486add6552ecd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
@@ -18,6 +18,6 @@ include "basic_2/conversion/cpc.ma".
 
 (* Main properties **********************************************************)
 
-theorem cpc_conf: ∀L,T0,T1,T2. L ⊢ T0 ⬌ T1 → L ⊢ T0 ⬌ T2 →
-                  ∃∃T. L ⊢ T1 ⬌ T & L ⊢ T2 ⬌ T.
+theorem cpc_conf: ∀L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌ T1 → ⦃G, L⦄ ⊢ T0 ⬌ T2 →
+                  ∃∃T. ⦃G, L⦄ ⊢ T1 ⬌ T & ⦃G, L⦄ ⊢ T2 ⬌ T.
 /3 width=3/ qed.