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

diff --git a/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/library/Fsub/part1a.ma
index 622b8f702..21fa35aa0 100644
--- a/helm/software/matita/library/Fsub/part1a.ma
+++ b/helm/software/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.