- pts_dummy/pts_dummy_new: non compiling parts commented out

[helm.git] / matita / matita / lib / pts_dummy / CC2FO_K_cube.ma

diff --git a/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma b/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma
index 814ce59fec6d9fa19476ab35ae2ec237030ec995..b70f731f1f54f64f3c63d86b842bd1bd2556c88f 100644 (file)
--- 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  
+*)