X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2FFsub%2Fpart1a.ma;h=21fa35aa0f9e1242c5f4ef406ffa15acf146e14c;hb=0d9db17cef4232805de6193f5ff0028a3c99d908;hp=622b8f702acf7adfc519663ad710f69fbbba4aaa;hpb=e32bda6193273d41ae80ba91fef6962008696a56;p=helm.git

diff --git a/matita/library/Fsub/part1a.ma b/matita/library/Fsub/part1a.ma
index 622b8f702..21fa35aa0 100644
--- a/matita/library/Fsub/part1a.ma
+++ b/matita/library/Fsub/part1a.ma
@@ -13,10 +13,10 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/Fsub/part1a/".
-include "library/logic/equality.ma".
-include "library/nat/nat.ma".
-include "library/datatypes/bool.ma".
-include "library/nat/compare.ma".
+include "logic/equality.ma".
+include "nat/nat.ma".
+include "datatypes/bool.ma".
+include "nat/compare.ma".
 include "Fsub/defn.ma".
 
 theorem JS_Refl : \forall T,G.(WFType G T) \to (WFEnv G) \to (JSubtype G T T).
@@ -377,4 +377,4 @@ theorem JS_narrow : \forall G1,G2,X,P,Q,T,U.
                        (JSubtype (G2 @ (mk_bound true X P :: G1)) T U).
 intros;elim (JS_trans_narrow (t_len Q));apply (H3 ? ? ? ? ? ? ? ? H H1);
 constructor 1;
-qed.
\ No newline at end of file
+qed.