Porting of setoids.ma from Coq continued.

[helm.git] / matita / library / Fsub / part1a.ma

diff --git a/matita/library/Fsub/part1a.ma b/matita/library/Fsub/part1a.ma
index 622b8f702acf7adfc519663ad710f69fbbba4aaa..21fa35aa0f9e1242c5f4ef406ffa15acf146e14c 100644 (file)
--- 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.