update in ground_2, static_2, basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cprs_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma
index bbc0b19a5c53644ec28643e75c0bb5919773a3ed..8446ee1f2878795673c054c480219a89740fa091 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma
@@ -20,10 +20,10 @@ include "basic_2/rt_computation/cpms_drops.ma".
 
 (* Basic_1: was: pr3_gen_lref *)
 (* Basic_2A1: was: cprs_inv_lref1 *)
-lemma cprs_inv_lref1_drops (h) (G): â\88\80L,T2,i. â¦\83G,Lâ¦\84 ⊢ #i ➡*[h] T2 →
+lemma cprs_inv_lref1_drops (h) (G): â\88\80L,T2,i. â\9dªG,Lâ\9d« ⊢ #i ➡*[h] T2 →
                                     ∨∨ T2 = #i
-                                     | ∃∃K,V1,T1. ⇩*[i] L ≘ K.ⓓV1 & ⦃G,K⦄ ⊢ V1 ➡*[h] T1 &
-                                                  ⇧*[↑i] T1 ≘ T2.
+                                     | ∃∃K,V1,T1. ⇩[i] L ≘ K.ⓓV1 & ❪G,K❫ ⊢ V1 ➡*[h] T1 &
+                                                  ⇧[↑i] T1 ≘ T2.
 #h #G #L #T2 #i #H elim (cpms_inv_lref1_drops … H) -H *
 [ /2 width=1 by or_introl/
 | /3 width=6 by ex3_3_intro, or_intror/