- notational change for cpg and cpx

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpg_simple.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
index 5dcf8ece0ffdff50a57f4da0c31bd06595481478..a53be69b04b218bad0b92569e7ddfb9fd3d051f1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
@@ -20,8 +20,8 @@ include "basic_2/rt_transition/cpg.ma".
 (* Properties with simple terms *********************************************)
 
 (* Note: the main property of simple terms *)
-lemma cpg_inv_appl1_simple: â\88\80c,h,G,L,V1,T1,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â\9e¡[c, h] U → 𝐒⦃T1⦄ →
-                            â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_appl1_simple: â\88\80c,h,G,L,V1,T1,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â¬\88[c, h] U → 𝐒⦃T1⦄ →
+                            â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
                                            U = ⓐV2.T2 & c = (↓cV)+cT.
 #c #h #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H *
 [ /2 width=8 by ex4_4_intro/