update in ground_2, static_2, basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
index 53f9d778d6ee580474db80b1fb81347ce937499d..a8b160cd122254356839d9a299adaf50cd132833 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_4_3.ma".
 include "ground_2/steps/rtc_ist_shift.ma".
 include "ground_2/steps/rtc_ist_plus.ma".
 include "ground_2/steps/rtc_ist_max.ma".
@@ -177,7 +178,7 @@ qed.
 lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
       ∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
 #h #n #G #L #l #X2 * #c #Hc #H elim (cpg_inv_gref1 … H) -H
-#H1 #H2 destruct /2 width=1 by conj/ 
+#H1 #H2 destruct /2 width=1 by conj/
 qed-.
 
 lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1):