X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fpts_dummy%2FCC2FO_K_cube.ma;fp=matita%2Fmatita%2Flib%2Fpts_dummy%2FCC2FO_K_cube.ma;h=b70f731f1f54f64f3c63d86b842bd1bd2556c88f;hb=dbd9f7d4de8286fdd54f4b5609576f33db1050a6;hp=814ce59fec6d9fa19476ab35ae2ec237030ec995;hpb=716338697e54d7a7e3602aabdecc2a8a639d683e;p=helm.git

diff --git a/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma b/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma
index 814ce59fe..b70f731f1 100644
--- a/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma
+++ b/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma
@@ -12,13 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "CC2FO_K.ma".
-include "cube.ma".
-include "inversion.ma".
-
+include "pts_dummy/CC2FO_K.ma".
+include "pts_dummy/cube.ma".
+include "pts_dummy/inversion.ma".
+(*
 (* The K interpretation in the λ-Cube *****************************************)
 
 lemma ki_type: ∀G,t,u. G ⊢_{CC} t : u → u = Sort 1 → 𝕂{G} ⊢_{FO} 𝕂{t}_[G] : u.
 #G #t #u #H elim H -H G t u
 [ #i #j * #_ @ax //
-| #G #A #i #HA #IHA #Heq  
\ No newline at end of file
+| #G #A #i #HA #IHA #Heq  
+*)