X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpt.ma;h=a8b160cd122254356839d9a299adaf50cd132833;hb=d8d00d6f6694155be5be486a8239f5953efe28b7;hp=53f9d778d6ee580474db80b1fb81347ce937499d;hpb=bfd440cc2a790741616cae6b375609c6bbdc3b24;p=helm.git

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 53f9d778d..a8b160cd1 100644
--- 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):