From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 21 Jul 2008 18:10:30 +0000 (+0000)
Subject: we implemented the support for generating ma files from mma files
X-Git-Tag: make_still_working~4903
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=662f191b09d1b9e3d13e4f9ee5c174c1ac08fadb;hp=deaa74701b73276ab7312911a56bee316c2ca110;p=helm.git

we implemented the support for generating ma files from mma files
---

diff --git a/helm/software/components/grafite_parser/dependenciesParser.ml b/helm/software/components/grafite_parser/dependenciesParser.ml
index 32ee44491..b44ad4994 100644
--- a/helm/software/components/grafite_parser/dependenciesParser.ml
+++ b/helm/software/components/grafite_parser/dependenciesParser.ml
@@ -31,10 +31,12 @@ exception UnableToInclude of string
 type dependency =
   | IncludeDep of string
   | UriDep of UriManager.uri
-  
+  | InlineDep of string
+
 let pp_dependency = function
   | IncludeDep str -> "include \"" ^ str ^ "\""
   | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
+  | InlineDep str -> "inline \"" ^ str ^ "\"" 
 
 let parse_dependencies lexbuf = 
   let tok_stream,_ =
@@ -56,6 +58,8 @@ let parse_dependencies lexbuf =
           true, (IncludeDep fname :: acc)
       | [< '("IDENT", "include'"); '("QSTRING", fname) >] ->
           true, (IncludeDep fname :: acc)
+      | [< '("IDENT", "inline"); '("IDENT", "procedural"); '("QSTRING", fname) >] ->
+          true, (InlineDep fname :: acc)
       | [< '("EOI", _) >] -> false, acc
       | [< 'tok >] -> true, acc
       | [<  >] -> false, acc) tok_stream
diff --git a/helm/software/components/grafite_parser/dependenciesParser.mli b/helm/software/components/grafite_parser/dependenciesParser.mli
index 1b4a03a71..57529966b 100644
--- a/helm/software/components/grafite_parser/dependenciesParser.mli
+++ b/helm/software/components/grafite_parser/dependenciesParser.mli
@@ -29,6 +29,7 @@ exception UnableToInclude of string
 type dependency =
   | IncludeDep of string
   | UriDep of UriManager.uri
+  | InlineDep of string
 
 val pp_dependency: dependency -> string
 
diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index 8b7bdb09f..f56ba5840 100644
--- a/helm/software/components/library/librarian.ml
+++ b/helm/software/components/library/librarian.ml
@@ -84,7 +84,7 @@ let load_root_file rootpath =
     lines
 ;;
 
-let find_root_for ~include_paths file = 
+let rec find_root_for ~include_paths file = 
  let include_paths = "" :: Sys.getcwd () :: include_paths in
  try 
    let path = HExtlib.find_in include_paths file in
@@ -108,10 +108,16 @@ let find_root_for ~include_paths file =
      HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
    ensure_trailing_slash root, remove_trailing_slash uri, path
  with Failure "find_in" -> 
-   HLog.error ("We are in: " ^ Sys.getcwd ());
-   HLog.error ("Unable to find: "^file^"\nPaths explored:");
-   List.iter (fun x -> HLog.error (" - "^x)) include_paths;
-   raise (NoRootFor file)
+   if Filename.check_suffix file ".ma" then begin
+      let mma = Filename.chop_suffix file ".ma" ^ ".mma" in
+      HLog.warn ("We look for: " ^ mma);
+      find_root_for ~include_paths mma
+   end else begin
+      HLog.error ("We are in: " ^ Sys.getcwd ());
+      HLog.error ("Unable to find: "^file^"\nPaths explored:");
+      List.iter (fun x -> HLog.error (" - "^x)) include_paths;
+      raise (NoRootFor file)
+   end
 ;;
 
 let mk_baseuri root extra =
diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt
index 8477d5640..ee77638cc 100644
--- a/helm/software/matita/.depend.opt
+++ b/helm/software/matita/.depend.opt
@@ -18,8 +18,8 @@ matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaWiki.cmx \
     matitaMisc.cmi matitaInit.cmi 
 matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaWiki.cmx \
     matitaMisc.cmx matitaInit.cmx 
-matitadep.cmo: matitaInit.cmi matitadep.cmi 
-matitadep.cmx: matitaInit.cmx matitadep.cmi 
+matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi 
+matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi 
 matitaEngine.cmo: matitaEngine.cmi 
 matitaEngine.cmx: matitaEngine.cmi 
 matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi 
@@ -34,10 +34,10 @@ matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
 matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
     matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \
     matitaExcPp.cmx matitaAutoGui.cmx buildTimeConf.cmx matitaGui.cmi 
-matitaInit.cmo: matitacLib.cmi matitaExcPp.cmi matitaEngine.cmi \
-    buildTimeConf.cmx matitaInit.cmi 
-matitaInit.cmx: matitacLib.cmx matitaExcPp.cmx matitaEngine.cmx \
-    buildTimeConf.cmx matitaInit.cmi 
+matitaInit.cmo: matitacLib.cmi matitaExcPp.cmi buildTimeConf.cmx \
+    matitaInit.cmi 
+matitaInit.cmx: matitacLib.cmx matitaExcPp.cmx buildTimeConf.cmx \
+    matitaInit.cmi 
 matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
     matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \
     buildTimeConf.cmx applyTransformation.cmi matitaMathView.cmi 
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend
deleted file mode 100644
index 52fc20094..000000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend
+++ /dev/null
@@ -1,8 +0,0 @@
-Base-2/ext/tactics.ma: Base-2/ext/tactics.mma Base-2/preamble.ma
-Base-2/ext/arith.ma: Base-2/ext/arith.mma Base-2/preamble.ma
-Base-2/types/defs.ma: Base-2/types/defs.mma Base-2/preamble.ma
-Base-2/types/props.ma: Base-2/types/props.mma Base-2/types/defs.ma
-Base-2/blt/defs.ma: Base-2/blt/defs.mma Base-2/preamble.ma
-Base-2/blt/props.ma: Base-2/blt/props.mma Base-2/blt/defs.ma
-Base-2/plist/defs.ma: Base-2/plist/defs.mma Base-2/preamble.ma
-Base-2/plist/props.ma: Base-2/plist/props.mma Base-2/plist/defs.ma
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends
deleted file mode 100644
index fd98f272c..000000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends
+++ /dev/null
@@ -1,8 +0,0 @@
-Base-2/ext/tactics.mma Base-2/preamble.ma Base-1/ext/tactics.ma
-Base-2/ext/arith.mma Base-2/preamble.ma Base-1/ext/arith.ma
-Base-2/types/defs.mma Base-2/preamble.ma Base-1/types/defs.ma
-Base-2/types/props.mma Base-2/preamble.ma Base-1/types/props.ma
-Base-2/blt/defs.mma Base-2/preamble.ma Base-1/blt/defs.ma
-Base-2/blt/props.mma Base-2/preamble.ma Base-1/blt/props.ma
-Base-2/plist/defs.mma Base-2/preamble.ma Base-1/plist/defs.ma
-Base-2/plist/props.mma Base-2/preamble.ma Base-1/plist/props.ma
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-2/.depend b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-2/.depend
deleted file mode 100644
index aa6d6dc8a..000000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-2/.depend
+++ /dev/null
@@ -1,216 +0,0 @@
-LambdaDelta-2/T/defs.ma: LambdaDelta-2/T/defs.mma LambdaDelta-2/preamble.ma
-LambdaDelta-2/T/props.ma: LambdaDelta-2/T/props.mma LambdaDelta-2/T/defs.ma
-LambdaDelta-2/T/dec.ma: LambdaDelta-2/T/dec.mma LambdaDelta-2/T/defs.ma
-LambdaDelta-2/s/defs.ma: LambdaDelta-2/s/defs.mma LambdaDelta-2/T/defs.ma
-LambdaDelta-2/s/props.ma: LambdaDelta-2/s/props.mma LambdaDelta-2/s/defs.ma
-LambdaDelta-2/tlist/defs.ma: LambdaDelta-2/tlist/defs.mma LambdaDelta-2/T/defs.ma
-LambdaDelta-2/tlist/props.ma: LambdaDelta-2/tlist/props.mma LambdaDelta-2/tlist/defs.ma
-LambdaDelta-2/tlt/defs.ma: LambdaDelta-2/tlt/defs.mma LambdaDelta-2/T/defs.ma
-LambdaDelta-2/tlt/props.ma: LambdaDelta-2/tlt/props.mma LambdaDelta-2/tlt/defs.ma
-LambdaDelta-2/iso/defs.ma: LambdaDelta-2/iso/defs.mma LambdaDelta-2/T/defs.ma
-LambdaDelta-2/iso/fwd.ma: LambdaDelta-2/iso/fwd.mma LambdaDelta-2/iso/defs.ma LambdaDelta-2/tlist/defs.ma
-LambdaDelta-2/iso/props.ma: LambdaDelta-2/iso/props.mma LambdaDelta-2/iso/fwd.ma
-LambdaDelta-2/C/defs.ma: LambdaDelta-2/C/defs.mma LambdaDelta-2/T/defs.ma
-LambdaDelta-2/C/props.ma: LambdaDelta-2/C/props.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/T/props.ma
-LambdaDelta-2/r/defs.ma: LambdaDelta-2/r/defs.mma LambdaDelta-2/T/defs.ma
-LambdaDelta-2/r/props.ma: LambdaDelta-2/r/props.mma LambdaDelta-2/r/defs.ma LambdaDelta-2/s/defs.ma
-LambdaDelta-2/clen/defs.ma: LambdaDelta-2/clen/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/s/defs.ma
-LambdaDelta-2/clen/getl.ma: LambdaDelta-2/clen/getl.mma LambdaDelta-2/clen/defs.ma LambdaDelta-2/getl/props.ma
-LambdaDelta-2/flt/defs.ma: LambdaDelta-2/flt/defs.mma LambdaDelta-2/C/defs.ma
-LambdaDelta-2/flt/props.ma: LambdaDelta-2/flt/props.mma LambdaDelta-2/flt/defs.ma LambdaDelta-2/C/props.ma
-LambdaDelta-2/app/defs.ma: LambdaDelta-2/app/defs.mma LambdaDelta-2/C/defs.ma
-LambdaDelta-2/lift/defs.ma: LambdaDelta-2/lift/defs.mma LambdaDelta-2/tlist/defs.ma LambdaDelta-2/s/defs.ma
-LambdaDelta-2/lift/fwd.ma: LambdaDelta-2/lift/fwd.mma LambdaDelta-2/lift/defs.ma
-LambdaDelta-2/lift/props.ma: LambdaDelta-2/lift/props.mma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/s/props.ma
-LambdaDelta-2/lift/tlt.ma: LambdaDelta-2/lift/tlt.mma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/tlt/props.ma
-LambdaDelta-2/lift1/defs.ma: LambdaDelta-2/lift1/defs.mma LambdaDelta-2/lift/defs.ma
-LambdaDelta-2/lift1/fwd.ma: LambdaDelta-2/lift1/fwd.mma LambdaDelta-2/lift1/defs.ma LambdaDelta-2/lift/fwd.ma
-LambdaDelta-2/lift1/props.ma: LambdaDelta-2/lift1/props.mma LambdaDelta-2/lift/props.ma LambdaDelta-2/drop1/defs.ma
-LambdaDelta-2/cnt/defs.ma: LambdaDelta-2/cnt/defs.mma LambdaDelta-2/T/defs.ma
-LambdaDelta-2/cnt/props.ma: LambdaDelta-2/cnt/props.mma LambdaDelta-2/cnt/defs.ma LambdaDelta-2/lift/fwd.ma
-LambdaDelta-2/drop/defs.ma: LambdaDelta-2/drop/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/lift/defs.ma LambdaDelta-2/r/defs.ma
-LambdaDelta-2/drop/fwd.ma: LambdaDelta-2/drop/fwd.mma LambdaDelta-2/drop/defs.ma
-LambdaDelta-2/drop/props.ma: LambdaDelta-2/drop/props.mma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/lift/props.ma LambdaDelta-2/r/props.ma
-LambdaDelta-2/drop1/defs.ma: LambdaDelta-2/drop1/defs.mma LambdaDelta-2/drop/defs.ma LambdaDelta-2/lift1/defs.ma
-LambdaDelta-2/drop1/fwd.ma: LambdaDelta-2/drop1/fwd.mma LambdaDelta-2/drop1/defs.ma
-LambdaDelta-2/drop1/props.ma: LambdaDelta-2/drop1/props.mma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/drop/props.ma LambdaDelta-2/getl/defs.ma
-LambdaDelta-2/drop1/getl.ma: LambdaDelta-2/drop1/getl.mma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/getl/drop.ma
-LambdaDelta-2/clear/defs.ma: LambdaDelta-2/clear/defs.mma LambdaDelta-2/C/defs.ma
-LambdaDelta-2/clear/fwd.ma: LambdaDelta-2/clear/fwd.mma LambdaDelta-2/clear/defs.ma
-LambdaDelta-2/clear/props.ma: LambdaDelta-2/clear/props.mma LambdaDelta-2/clear/fwd.ma
-LambdaDelta-2/clear/drop.ma: LambdaDelta-2/clear/drop.mma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/drop/fwd.ma
-LambdaDelta-2/getl/defs.ma: LambdaDelta-2/getl/defs.mma LambdaDelta-2/drop/defs.ma LambdaDelta-2/clear/defs.ma
-LambdaDelta-2/getl/fwd.ma: LambdaDelta-2/getl/fwd.mma LambdaDelta-2/getl/defs.ma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/clear/fwd.ma
-LambdaDelta-2/getl/props.ma: LambdaDelta-2/getl/props.mma LambdaDelta-2/getl/fwd.ma LambdaDelta-2/drop/props.ma LambdaDelta-2/clear/props.ma
-LambdaDelta-2/getl/clear.ma: LambdaDelta-2/getl/clear.mma LambdaDelta-2/getl/props.ma LambdaDelta-2/clear/drop.ma
-LambdaDelta-2/getl/drop.ma: LambdaDelta-2/getl/drop.mma LambdaDelta-2/getl/props.ma LambdaDelta-2/clear/drop.ma
-LambdaDelta-2/getl/getl.ma: LambdaDelta-2/getl/getl.mma LambdaDelta-2/getl/drop.ma LambdaDelta-2/getl/clear.ma
-LambdaDelta-2/getl/dec.ma: LambdaDelta-2/getl/dec.mma LambdaDelta-2/getl/props.ma
-LambdaDelta-2/getl/flt.ma: LambdaDelta-2/getl/flt.mma LambdaDelta-2/getl/fwd.ma LambdaDelta-2/clear/props.ma LambdaDelta-2/flt/props.ma
-LambdaDelta-2/cimp/defs.ma: LambdaDelta-2/cimp/defs.mma LambdaDelta-2/getl/defs.ma
-LambdaDelta-2/cimp/props.ma: LambdaDelta-2/cimp/props.mma LambdaDelta-2/cimp/defs.ma LambdaDelta-2/getl/getl.ma
-LambdaDelta-2/csubv/defs.ma: LambdaDelta-2/csubv/defs.mma LambdaDelta-2/C/defs.ma
-LambdaDelta-2/csubv/props.ma: LambdaDelta-2/csubv/props.mma LambdaDelta-2/csubv/defs.ma LambdaDelta-2/T/props.ma
-LambdaDelta-2/csubv/drop.ma: LambdaDelta-2/csubv/drop.mma LambdaDelta-2/csubv/props.ma LambdaDelta-2/drop/fwd.ma
-LambdaDelta-2/csubv/clear.ma: LambdaDelta-2/csubv/clear.mma LambdaDelta-2/csubv/defs.ma LambdaDelta-2/clear/fwd.ma
-LambdaDelta-2/csubv/getl.ma: LambdaDelta-2/csubv/getl.mma LambdaDelta-2/csubv/clear.ma LambdaDelta-2/csubv/drop.ma LambdaDelta-2/getl/fwd.ma
-LambdaDelta-2/subst0/defs.ma: LambdaDelta-2/subst0/defs.mma LambdaDelta-2/lift/defs.ma
-LambdaDelta-2/subst0/fwd.ma: LambdaDelta-2/subst0/fwd.mma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/lift/props.ma
-LambdaDelta-2/subst0/props.ma: LambdaDelta-2/subst0/props.mma LambdaDelta-2/subst0/fwd.ma
-LambdaDelta-2/subst0/subst0.ma: LambdaDelta-2/subst0/subst0.mma LambdaDelta-2/subst0/props.ma
-LambdaDelta-2/subst0/tlt.ma: LambdaDelta-2/subst0/tlt.mma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/lift/props.ma LambdaDelta-2/lift/tlt.ma
-LambdaDelta-2/subst0/dec.ma: LambdaDelta-2/subst0/dec.mma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/lift/props.ma
-LambdaDelta-2/subst/defs.ma: LambdaDelta-2/subst/defs.mma LambdaDelta-2/lift/defs.ma
-LambdaDelta-2/subst/fwd.ma: LambdaDelta-2/subst/fwd.mma LambdaDelta-2/subst/defs.ma
-LambdaDelta-2/subst/props.ma: LambdaDelta-2/subst/props.mma LambdaDelta-2/subst/fwd.ma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/lift/props.ma
-LambdaDelta-2/subst1/defs.ma: LambdaDelta-2/subst1/defs.mma LambdaDelta-2/subst0/defs.ma
-LambdaDelta-2/subst1/fwd.ma: LambdaDelta-2/subst1/fwd.mma LambdaDelta-2/subst1/defs.ma LambdaDelta-2/subst0/props.ma
-LambdaDelta-2/subst1/props.ma: LambdaDelta-2/subst1/props.mma LambdaDelta-2/subst1/defs.ma LambdaDelta-2/subst0/props.ma
-LambdaDelta-2/subst1/subst1.ma: LambdaDelta-2/subst1/subst1.mma LambdaDelta-2/subst1/fwd.ma LambdaDelta-2/subst0/subst0.ma
-LambdaDelta-2/csubst0/defs.ma: LambdaDelta-2/csubst0/defs.mma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/C/defs.ma
-LambdaDelta-2/csubst0/fwd.ma: LambdaDelta-2/csubst0/fwd.mma LambdaDelta-2/csubst0/defs.ma
-LambdaDelta-2/csubst0/props.ma: LambdaDelta-2/csubst0/props.mma LambdaDelta-2/csubst0/defs.ma
-LambdaDelta-2/csubst0/drop.ma: LambdaDelta-2/csubst0/drop.mma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/s/props.ma
-LambdaDelta-2/csubst0/clear.ma: LambdaDelta-2/csubst0/clear.mma LambdaDelta-2/csubst0/props.ma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/clear/fwd.ma
-LambdaDelta-2/csubst0/getl.ma: LambdaDelta-2/csubst0/getl.mma LambdaDelta-2/csubst0/clear.ma LambdaDelta-2/csubst0/drop.ma LambdaDelta-2/getl/fwd.ma
-LambdaDelta-2/csubst1/defs.ma: LambdaDelta-2/csubst1/defs.mma LambdaDelta-2/csubst0/defs.ma
-LambdaDelta-2/csubst1/fwd.ma: LambdaDelta-2/csubst1/fwd.mma LambdaDelta-2/csubst1/defs.ma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/subst1/props.ma
-LambdaDelta-2/csubst1/props.ma: LambdaDelta-2/csubst1/props.mma LambdaDelta-2/csubst1/defs.ma LambdaDelta-2/subst1/defs.ma
-LambdaDelta-2/csubst1/getl.ma: LambdaDelta-2/csubst1/getl.mma LambdaDelta-2/csubst1/props.ma LambdaDelta-2/csubst0/getl.ma LambdaDelta-2/subst1/props.ma LambdaDelta-2/drop/props.ma
-LambdaDelta-2/fsubst0/defs.ma: LambdaDelta-2/fsubst0/defs.mma LambdaDelta-2/csubst0/defs.ma
-LambdaDelta-2/fsubst0/fwd.ma: LambdaDelta-2/fsubst0/fwd.mma LambdaDelta-2/fsubst0/defs.ma
-LambdaDelta-2/G/defs.ma: LambdaDelta-2/G/defs.mma LambdaDelta-2/preamble.ma
-LambdaDelta-2/next_plus/defs.ma: LambdaDelta-2/next_plus/defs.mma LambdaDelta-2/G/defs.ma
-LambdaDelta-2/next_plus/props.ma: LambdaDelta-2/next_plus/props.mma LambdaDelta-2/next_plus/defs.ma
-LambdaDelta-2/sty0/defs.ma: LambdaDelta-2/sty0/defs.mma LambdaDelta-2/G/defs.ma LambdaDelta-2/getl/defs.ma
-LambdaDelta-2/sty0/fwd.ma: LambdaDelta-2/sty0/fwd.mma LambdaDelta-2/sty0/defs.ma
-LambdaDelta-2/sty0/props.ma: LambdaDelta-2/sty0/props.mma LambdaDelta-2/sty0/defs.ma LambdaDelta-2/getl/drop.ma
-LambdaDelta-2/sty1/defs.ma: LambdaDelta-2/sty1/defs.mma LambdaDelta-2/sty0/defs.ma
-LambdaDelta-2/sty1/props.ma: LambdaDelta-2/sty1/props.mma LambdaDelta-2/sty1/defs.ma LambdaDelta-2/sty0/props.ma
-LambdaDelta-2/sty1/cnt.ma: LambdaDelta-2/sty1/cnt.mma LambdaDelta-2/sty1/props.ma LambdaDelta-2/cnt/props.ma
-LambdaDelta-2/A/defs.ma: LambdaDelta-2/A/defs.mma LambdaDelta-2/preamble.ma
-LambdaDelta-2/asucc/defs.ma: LambdaDelta-2/asucc/defs.mma LambdaDelta-2/A/defs.ma LambdaDelta-2/G/defs.ma
-LambdaDelta-2/asucc/fwd.ma: LambdaDelta-2/asucc/fwd.mma LambdaDelta-2/asucc/defs.ma
-LambdaDelta-2/aplus/defs.ma: LambdaDelta-2/aplus/defs.mma LambdaDelta-2/asucc/defs.ma
-LambdaDelta-2/aplus/props.ma: LambdaDelta-2/aplus/props.mma LambdaDelta-2/aplus/defs.ma LambdaDelta-2/next_plus/props.ma
-LambdaDelta-2/leq/defs.ma: LambdaDelta-2/leq/defs.mma LambdaDelta-2/aplus/defs.ma
-LambdaDelta-2/leq/fwd.ma: LambdaDelta-2/leq/fwd.mma LambdaDelta-2/leq/defs.ma
-LambdaDelta-2/leq/props.ma: LambdaDelta-2/leq/props.mma LambdaDelta-2/leq/fwd.ma LambdaDelta-2/aplus/props.ma
-LambdaDelta-2/leq/asucc.ma: LambdaDelta-2/leq/asucc.mma LambdaDelta-2/leq/props.ma
-LambdaDelta-2/llt/defs.ma: LambdaDelta-2/llt/defs.mma LambdaDelta-2/A/defs.ma
-LambdaDelta-2/llt/props.ma: LambdaDelta-2/llt/props.mma LambdaDelta-2/llt/defs.ma LambdaDelta-2/leq/defs.ma
-LambdaDelta-2/aprem/defs.ma: LambdaDelta-2/aprem/defs.mma LambdaDelta-2/A/defs.ma
-LambdaDelta-2/aprem/fwd.ma: LambdaDelta-2/aprem/fwd.mma LambdaDelta-2/aprem/defs.ma
-LambdaDelta-2/aprem/props.ma: LambdaDelta-2/aprem/props.mma LambdaDelta-2/aprem/fwd.ma LambdaDelta-2/leq/defs.ma
-LambdaDelta-2/ex0/defs.ma: LambdaDelta-2/ex0/defs.mma LambdaDelta-2/A/defs.ma LambdaDelta-2/G/defs.ma
-LambdaDelta-2/ex0/props.ma: LambdaDelta-2/ex0/props.mma LambdaDelta-2/ex0/defs.ma LambdaDelta-2/leq/defs.ma LambdaDelta-2/aplus/props.ma
-LambdaDelta-2/arity/defs.ma: LambdaDelta-2/arity/defs.mma LambdaDelta-2/leq/defs.ma LambdaDelta-2/getl/defs.ma
-LambdaDelta-2/arity/fwd.ma: LambdaDelta-2/arity/fwd.mma LambdaDelta-2/arity/defs.ma LambdaDelta-2/leq/asucc.ma LambdaDelta-2/getl/drop.ma
-LambdaDelta-2/arity/props.ma: LambdaDelta-2/arity/props.mma LambdaDelta-2/arity/fwd.ma
-LambdaDelta-2/arity/subst0.ma: LambdaDelta-2/arity/subst0.mma LambdaDelta-2/arity/props.ma LambdaDelta-2/fsubst0/fwd.ma LambdaDelta-2/csubst0/getl.ma LambdaDelta-2/subst0/dec.ma LambdaDelta-2/subst0/fwd.ma LambdaDelta-2/getl/getl.ma
-LambdaDelta-2/arity/lift1.ma: LambdaDelta-2/arity/lift1.mma LambdaDelta-2/arity/props.ma LambdaDelta-2/drop1/fwd.ma
-LambdaDelta-2/arity/cimp.ma: LambdaDelta-2/arity/cimp.mma LambdaDelta-2/arity/defs.ma LambdaDelta-2/cimp/props.ma
-LambdaDelta-2/arity/aprem.ma: LambdaDelta-2/arity/aprem.mma LambdaDelta-2/arity/props.ma LambdaDelta-2/arity/cimp.ma LambdaDelta-2/aprem/props.ma
-LambdaDelta-2/pr0/defs.ma: LambdaDelta-2/pr0/defs.mma LambdaDelta-2/subst0/defs.ma
-LambdaDelta-2/pr0/fwd.ma: LambdaDelta-2/pr0/fwd.mma LambdaDelta-2/pr0/props.ma
-LambdaDelta-2/pr0/props.ma: LambdaDelta-2/pr0/props.mma LambdaDelta-2/pr0/defs.ma LambdaDelta-2/subst0/subst0.ma
-LambdaDelta-2/pr0/pr0.ma: LambdaDelta-2/pr0/pr0.mma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/lift/tlt.ma
-LambdaDelta-2/pr0/subst1.ma: LambdaDelta-2/pr0/subst1.mma LambdaDelta-2/pr0/props.ma LambdaDelta-2/subst1/defs.ma
-LambdaDelta-2/pr0/dec.ma: LambdaDelta-2/pr0/dec.mma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/subst0/dec.ma LambdaDelta-2/T/dec.ma LambdaDelta-2/T/props.ma
-LambdaDelta-2/pr1/defs.ma: LambdaDelta-2/pr1/defs.mma LambdaDelta-2/pr0/defs.ma
-LambdaDelta-2/pr1/props.ma: LambdaDelta-2/pr1/props.mma LambdaDelta-2/pr1/defs.ma LambdaDelta-2/pr0/subst1.ma LambdaDelta-2/subst1/props.ma LambdaDelta-2/T/props.ma
-LambdaDelta-2/pr1/pr1.ma: LambdaDelta-2/pr1/pr1.mma LambdaDelta-2/pr1/props.ma LambdaDelta-2/pr0/pr0.ma
-LambdaDelta-2/wcpr0/defs.ma: LambdaDelta-2/wcpr0/defs.mma LambdaDelta-2/pr0/defs.ma LambdaDelta-2/C/defs.ma
-LambdaDelta-2/wcpr0/fwd.ma: LambdaDelta-2/wcpr0/fwd.mma LambdaDelta-2/wcpr0/defs.ma
-LambdaDelta-2/wcpr0/getl.ma: LambdaDelta-2/wcpr0/getl.mma LambdaDelta-2/wcpr0/defs.ma LambdaDelta-2/getl/props.ma
-LambdaDelta-2/pr2/defs.ma: LambdaDelta-2/pr2/defs.mma LambdaDelta-2/pr0/defs.ma LambdaDelta-2/getl/defs.ma
-LambdaDelta-2/pr2/fwd.ma: LambdaDelta-2/pr2/fwd.mma LambdaDelta-2/pr2/defs.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/getl/clear.ma
-LambdaDelta-2/pr2/props.ma: LambdaDelta-2/pr2/props.mma LambdaDelta-2/pr2/defs.ma LambdaDelta-2/pr0/props.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/getl/clear.ma
-LambdaDelta-2/pr2/clen.ma: LambdaDelta-2/pr2/clen.mma LambdaDelta-2/pr2/props.ma LambdaDelta-2/clen/getl.ma
-LambdaDelta-2/pr2/pr2.ma: LambdaDelta-2/pr2/pr2.mma LambdaDelta-2/pr2/defs.ma LambdaDelta-2/pr0/pr0.ma LambdaDelta-2/getl/props.ma
-LambdaDelta-2/pr2/subst1.ma: LambdaDelta-2/pr2/subst1.mma LambdaDelta-2/pr2/defs.ma LambdaDelta-2/pr0/subst1.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/csubst1/getl.ma LambdaDelta-2/csubst1/fwd.ma LambdaDelta-2/subst1/subst1.ma LambdaDelta-2/getl/drop.ma
-LambdaDelta-2/pr3/defs.ma: LambdaDelta-2/pr3/defs.mma LambdaDelta-2/pr2/defs.ma
-LambdaDelta-2/pr3/pr1.ma: LambdaDelta-2/pr3/pr1.mma LambdaDelta-2/pr3/defs.ma LambdaDelta-2/pr1/defs.ma
-LambdaDelta-2/pr3/props.ma: LambdaDelta-2/pr3/props.mma LambdaDelta-2/pr3/pr1.ma LambdaDelta-2/pr2/props.ma LambdaDelta-2/pr1/props.ma
-LambdaDelta-2/pr3/fwd.ma: LambdaDelta-2/pr3/fwd.mma LambdaDelta-2/pr3/props.ma LambdaDelta-2/pr2/fwd.ma
-LambdaDelta-2/pr3/wcpr0.ma: LambdaDelta-2/pr3/wcpr0.mma LambdaDelta-2/pr3/props.ma LambdaDelta-2/wcpr0/getl.ma
-LambdaDelta-2/pr3/pr3.ma: LambdaDelta-2/pr3/pr3.mma LambdaDelta-2/pr3/props.ma LambdaDelta-2/pr2/pr2.ma
-LambdaDelta-2/pr3/subst1.ma: LambdaDelta-2/pr3/subst1.mma LambdaDelta-2/pr3/defs.ma LambdaDelta-2/pr2/subst1.ma
-LambdaDelta-2/pr3/iso.ma: LambdaDelta-2/pr3/iso.mma LambdaDelta-2/pr3/fwd.ma LambdaDelta-2/iso/props.ma LambdaDelta-2/tlist/props.ma
-LambdaDelta-2/csuba/defs.ma: LambdaDelta-2/csuba/defs.mma LambdaDelta-2/arity/defs.ma
-LambdaDelta-2/csuba/fwd.ma: LambdaDelta-2/csuba/fwd.mma LambdaDelta-2/csuba/defs.ma
-LambdaDelta-2/csuba/props.ma: LambdaDelta-2/csuba/props.mma LambdaDelta-2/csuba/defs.ma
-LambdaDelta-2/csuba/clear.ma: LambdaDelta-2/csuba/clear.mma LambdaDelta-2/csuba/defs.ma LambdaDelta-2/clear/fwd.ma
-LambdaDelta-2/csuba/drop.ma: LambdaDelta-2/csuba/drop.mma LambdaDelta-2/csuba/fwd.ma LambdaDelta-2/drop/fwd.ma
-LambdaDelta-2/csuba/getl.ma: LambdaDelta-2/csuba/getl.mma LambdaDelta-2/csuba/drop.ma LambdaDelta-2/csuba/clear.ma LambdaDelta-2/getl/clear.ma
-LambdaDelta-2/csuba/arity.ma: LambdaDelta-2/csuba/arity.mma LambdaDelta-2/csuba/getl.ma LambdaDelta-2/csuba/props.ma LambdaDelta-2/arity/props.ma LambdaDelta-2/csubv/getl.ma
-LambdaDelta-2/arity/pr3.ma: LambdaDelta-2/arity/pr3.mma LambdaDelta-2/csuba/arity.ma LambdaDelta-2/pr3/defs.ma LambdaDelta-2/pr1/defs.ma LambdaDelta-2/wcpr0/getl.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/arity/subst0.ma
-LambdaDelta-2/nf2/defs.ma: LambdaDelta-2/nf2/defs.mma LambdaDelta-2/pr2/defs.ma
-LambdaDelta-2/nf2/fwd.ma: LambdaDelta-2/nf2/fwd.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/clen.ma LambdaDelta-2/subst0/dec.ma LambdaDelta-2/T/props.ma
-LambdaDelta-2/nf2/props.ma: LambdaDelta-2/nf2/props.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/fwd.ma
-LambdaDelta-2/nf2/arity.ma: LambdaDelta-2/nf2/arity.mma LambdaDelta-2/nf2/fwd.ma LambdaDelta-2/arity/subst0.ma
-LambdaDelta-2/nf2/pr3.ma: LambdaDelta-2/nf2/pr3.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr3/pr3.ma
-LambdaDelta-2/nf2/lift1.ma: LambdaDelta-2/nf2/lift1.mma LambdaDelta-2/nf2/props.ma LambdaDelta-2/drop1/fwd.ma
-LambdaDelta-2/nf2/iso.ma: LambdaDelta-2/nf2/iso.mma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/pr3/fwd.ma LambdaDelta-2/iso/props.ma
-LambdaDelta-2/ex2/defs.ma: LambdaDelta-2/ex2/defs.mma LambdaDelta-2/C/defs.ma
-LambdaDelta-2/ex2/props.ma: LambdaDelta-2/ex2/props.mma LambdaDelta-2/ex2/defs.ma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/fwd.ma LambdaDelta-2/arity/fwd.ma
-LambdaDelta-2/nf2/dec.ma: LambdaDelta-2/nf2/dec.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/clen.ma LambdaDelta-2/pr2/fwd.ma LambdaDelta-2/pr0/dec.ma LambdaDelta-2/C/props.ma
-LambdaDelta-2/sn3/defs.ma: LambdaDelta-2/sn3/defs.mma LambdaDelta-2/pr3/defs.ma
-LambdaDelta-2/sn3/fwd.ma: LambdaDelta-2/sn3/fwd.mma LambdaDelta-2/sn3/defs.ma LambdaDelta-2/pr3/props.ma
-LambdaDelta-2/sn3/nf2.ma: LambdaDelta-2/sn3/nf2.mma LambdaDelta-2/sn3/defs.ma LambdaDelta-2/nf2/dec.ma LambdaDelta-2/nf2/pr3.ma
-LambdaDelta-2/sn3/props.ma: LambdaDelta-2/sn3/props.mma LambdaDelta-2/sn3/nf2.ma LambdaDelta-2/sn3/fwd.ma LambdaDelta-2/nf2/iso.ma LambdaDelta-2/pr3/iso.ma
-LambdaDelta-2/sn3/lift1.ma: LambdaDelta-2/sn3/lift1.mma LambdaDelta-2/sn3/props.ma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/lift1/fwd.ma
-LambdaDelta-2/sc3/defs.ma: LambdaDelta-2/sc3/defs.mma LambdaDelta-2/sn3/defs.ma LambdaDelta-2/arity/defs.ma LambdaDelta-2/drop1/defs.ma
-LambdaDelta-2/sc3/props.ma: LambdaDelta-2/sc3/props.mma LambdaDelta-2/sc3/defs.ma LambdaDelta-2/sn3/lift1.ma LambdaDelta-2/nf2/lift1.ma LambdaDelta-2/csuba/arity.ma LambdaDelta-2/arity/lift1.ma LambdaDelta-2/arity/aprem.ma LambdaDelta-2/llt/props.ma LambdaDelta-2/drop1/getl.ma LambdaDelta-2/drop1/props.ma LambdaDelta-2/lift1/props.ma
-LambdaDelta-2/csubc/defs.ma: LambdaDelta-2/csubc/defs.mma LambdaDelta-2/sc3/defs.ma
-LambdaDelta-2/csubc/fwd.ma: LambdaDelta-2/csubc/fwd.mma LambdaDelta-2/csubc/defs.ma
-LambdaDelta-2/csubc/props.ma: LambdaDelta-2/csubc/props.mma LambdaDelta-2/csubc/defs.ma LambdaDelta-2/sc3/props.ma
-LambdaDelta-2/csubc/csuba.ma: LambdaDelta-2/csubc/csuba.mma LambdaDelta-2/csubc/defs.ma LambdaDelta-2/sc3/props.ma
-LambdaDelta-2/csubc/drop.ma: LambdaDelta-2/csubc/drop.mma LambdaDelta-2/csubc/fwd.ma LambdaDelta-2/sc3/props.ma
-LambdaDelta-2/csubc/drop1.ma: LambdaDelta-2/csubc/drop1.mma LambdaDelta-2/csubc/drop.ma
-LambdaDelta-2/csubc/clear.ma: LambdaDelta-2/csubc/clear.mma LambdaDelta-2/csubc/fwd.ma
-LambdaDelta-2/csubc/getl.ma: LambdaDelta-2/csubc/getl.mma LambdaDelta-2/csubc/drop.ma LambdaDelta-2/csubc/clear.ma
-LambdaDelta-2/csubc/arity.ma: LambdaDelta-2/csubc/arity.mma LambdaDelta-2/csubc/csuba.ma
-LambdaDelta-2/sc3/arity.ma: LambdaDelta-2/sc3/arity.mma LambdaDelta-2/csubc/arity.ma LambdaDelta-2/csubc/getl.ma LambdaDelta-2/csubc/drop1.ma LambdaDelta-2/csubc/props.ma
-LambdaDelta-2/pc1/defs.ma: LambdaDelta-2/pc1/defs.mma LambdaDelta-2/pr1/defs.ma
-LambdaDelta-2/pc1/props.ma: LambdaDelta-2/pc1/props.mma LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pr1/pr1.ma
-LambdaDelta-2/pc3/defs.ma: LambdaDelta-2/pc3/defs.mma LambdaDelta-2/pr3/defs.ma
-LambdaDelta-2/pc3/props.ma: LambdaDelta-2/pc3/props.mma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/pr3/pr3.ma
-LambdaDelta-2/pc3/pc1.ma: LambdaDelta-2/pc3/pc1.mma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pr3/pr1.ma
-LambdaDelta-2/pc3/nf2.ma: LambdaDelta-2/pc3/nf2.mma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/nf2/pr3.ma
-LambdaDelta-2/pc3/wcpr0.ma: LambdaDelta-2/pc3/wcpr0.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/wcpr0/getl.ma
-LambdaDelta-2/pc3/left.ma: LambdaDelta-2/pc3/left.mma LambdaDelta-2/pc3/props.ma
-LambdaDelta-2/pc3/fwd.ma: LambdaDelta-2/pc3/fwd.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/pr3/fwd.ma
-LambdaDelta-2/pc3/fsubst0.ma: LambdaDelta-2/pc3/fsubst0.mma LambdaDelta-2/pc3/left.ma LambdaDelta-2/fsubst0/defs.ma LambdaDelta-2/csubst0/getl.ma
-LambdaDelta-2/pc3/subst1.ma: LambdaDelta-2/pc3/subst1.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/pr3/subst1.ma
-LambdaDelta-2/ty3/defs.ma: LambdaDelta-2/ty3/defs.mma LambdaDelta-2/G/defs.ma LambdaDelta-2/pc3/defs.ma
-LambdaDelta-2/ty3/fwd.ma: LambdaDelta-2/ty3/fwd.mma LambdaDelta-2/ty3/defs.ma LambdaDelta-2/pc3/props.ma
-LambdaDelta-2/ex1/defs.ma: LambdaDelta-2/ex1/defs.mma LambdaDelta-2/C/defs.ma
-LambdaDelta-2/ex1/props.ma: LambdaDelta-2/ex1/props.mma LambdaDelta-2/ex1/defs.ma LambdaDelta-2/ty3/fwd.ma LambdaDelta-2/pc3/fwd.ma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/nf2/props.ma LambdaDelta-2/arity/defs.ma LambdaDelta-2/leq/props.ma
-LambdaDelta-2/ty3/props.ma: LambdaDelta-2/ty3/props.mma LambdaDelta-2/ty3/fwd.ma LambdaDelta-2/pc3/fwd.ma
-LambdaDelta-2/ty3/fsubst0.ma: LambdaDelta-2/ty3/fsubst0.mma LambdaDelta-2/ty3/props.ma LambdaDelta-2/pc3/fsubst0.ma LambdaDelta-2/getl/getl.ma
-LambdaDelta-2/ty3/subst1.ma: LambdaDelta-2/ty3/subst1.mma LambdaDelta-2/ty3/props.ma LambdaDelta-2/pc3/subst1.ma LambdaDelta-2/getl/getl.ma
-LambdaDelta-2/csubt/defs.ma: LambdaDelta-2/csubt/defs.mma LambdaDelta-2/ty3/defs.ma
-LambdaDelta-2/csubt/fwd.ma: LambdaDelta-2/csubt/fwd.mma LambdaDelta-2/csubt/defs.ma
-LambdaDelta-2/csubt/props.ma: LambdaDelta-2/csubt/props.mma LambdaDelta-2/csubt/defs.ma
-LambdaDelta-2/csubt/clear.ma: LambdaDelta-2/csubt/clear.mma LambdaDelta-2/csubt/defs.ma LambdaDelta-2/clear/fwd.ma
-LambdaDelta-2/csubt/drop.ma: LambdaDelta-2/csubt/drop.mma LambdaDelta-2/csubt/fwd.ma LambdaDelta-2/drop/fwd.ma
-LambdaDelta-2/csubt/getl.ma: LambdaDelta-2/csubt/getl.mma LambdaDelta-2/csubt/clear.ma LambdaDelta-2/csubt/drop.ma LambdaDelta-2/getl/clear.ma
-LambdaDelta-2/csubt/pc3.ma: LambdaDelta-2/csubt/pc3.mma LambdaDelta-2/csubt/getl.ma LambdaDelta-2/pc3/left.ma
-LambdaDelta-2/csubt/ty3.ma: LambdaDelta-2/csubt/ty3.mma LambdaDelta-2/csubt/pc3.ma LambdaDelta-2/csubt/props.ma
-LambdaDelta-2/ty3/pr3.ma: LambdaDelta-2/ty3/pr3.mma LambdaDelta-2/csubt/ty3.ma LambdaDelta-2/ty3/subst1.ma LambdaDelta-2/ty3/fsubst0.ma LambdaDelta-2/pc3/pc1.ma LambdaDelta-2/pc3/wcpr0.ma LambdaDelta-2/pc1/props.ma
-LambdaDelta-2/ty3/pr3_props.ma: LambdaDelta-2/ty3/pr3_props.mma LambdaDelta-2/ty3/pr3.ma
-LambdaDelta-2/ty3/sty0.ma: LambdaDelta-2/ty3/sty0.mma LambdaDelta-2/ty3/pr3_props.ma LambdaDelta-2/sty0/fwd.ma
-LambdaDelta-2/ty3/arity.ma: LambdaDelta-2/ty3/arity.mma LambdaDelta-2/ty3/pr3_props.ma LambdaDelta-2/arity/pr3.ma LambdaDelta-2/asucc/fwd.ma
-LambdaDelta-2/ty3/arity_props.ma: LambdaDelta-2/ty3/arity_props.mma LambdaDelta-2/ty3/arity.ma LambdaDelta-2/sc3/arity.ma
-LambdaDelta-2/csubt/csuba.ma: LambdaDelta-2/csubt/csuba.mma LambdaDelta-2/ty3/arity.ma
-LambdaDelta-2/ty3/fwd_nf2.ma: LambdaDelta-2/ty3/fwd_nf2.mma LambdaDelta-2/ty3/arity_props.ma LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/nf2/fwd.ma
-LambdaDelta-2/ty3/nf2.ma: LambdaDelta-2/ty3/nf2.mma LambdaDelta-2/ty3/arity.ma LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/nf2/arity.ma
-LambdaDelta-2/pc3/dec.ma: LambdaDelta-2/pc3/dec.mma LambdaDelta-2/ty3/arity_props.ma LambdaDelta-2/nf2/fwd.ma
-LambdaDelta-2/ty3/dec.ma: LambdaDelta-2/ty3/dec.mma LambdaDelta-2/pc3/dec.ma LambdaDelta-2/getl/flt.ma LambdaDelta-2/getl/dec.ma
-LambdaDelta-2/wf3/defs.ma: LambdaDelta-2/wf3/defs.mma LambdaDelta-2/ty3/defs.ma
-LambdaDelta-2/wf3/fwd.ma: LambdaDelta-2/wf3/fwd.mma LambdaDelta-2/wf3/defs.ma
-LambdaDelta-2/wf3/clear.ma: LambdaDelta-2/wf3/clear.mma LambdaDelta-2/wf3/fwd.ma
-LambdaDelta-2/wf3/getl.ma: LambdaDelta-2/wf3/getl.mma LambdaDelta-2/wf3/clear.ma LambdaDelta-2/ty3/dec.ma
-LambdaDelta-2/wf3/ty3.ma: LambdaDelta-2/wf3/ty3.mma LambdaDelta-2/wf3/getl.ma
-LambdaDelta-2/wf3/props.ma: LambdaDelta-2/wf3/props.mma LambdaDelta-2/wf3/ty3.ma LambdaDelta-2/app/defs.ma
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-2/depends b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-2/depends
deleted file mode 100644
index 8c376eb2a..000000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-2/depends
+++ /dev/null
@@ -1,216 +0,0 @@
-LambdaDelta-2/T/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/T/defs.ma
-LambdaDelta-2/T/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/T/props.ma
-LambdaDelta-2/T/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/T/dec.ma
-LambdaDelta-2/s/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/s/defs.ma
-LambdaDelta-2/s/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/s/props.ma
-LambdaDelta-2/tlist/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/tlist/defs.ma
-LambdaDelta-2/tlist/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/tlist/props.ma
-LambdaDelta-2/tlt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/tlt/defs.ma
-LambdaDelta-2/tlt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/tlt/props.ma
-LambdaDelta-2/iso/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/iso/defs.ma
-LambdaDelta-2/iso/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/iso/fwd.ma
-LambdaDelta-2/iso/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/iso/props.ma
-LambdaDelta-2/C/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/C/defs.ma
-LambdaDelta-2/C/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/C/props.ma
-LambdaDelta-2/r/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/r/defs.ma
-LambdaDelta-2/r/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/r/props.ma
-LambdaDelta-2/clen/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clen/defs.ma
-LambdaDelta-2/clen/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clen/getl.ma
-LambdaDelta-2/flt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/flt/defs.ma
-LambdaDelta-2/flt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/flt/props.ma
-LambdaDelta-2/app/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/app/defs.ma
-LambdaDelta-2/lift/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift/defs.ma
-LambdaDelta-2/lift/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift/fwd.ma
-LambdaDelta-2/lift/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift/props.ma
-LambdaDelta-2/lift/tlt.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift/tlt.ma
-LambdaDelta-2/lift1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift1/defs.ma
-LambdaDelta-2/lift1/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift1/fwd.ma
-LambdaDelta-2/lift1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift1/props.ma
-LambdaDelta-2/cnt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/cnt/defs.ma
-LambdaDelta-2/cnt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/cnt/props.ma
-LambdaDelta-2/drop/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop/defs.ma
-LambdaDelta-2/drop/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop/fwd.ma
-LambdaDelta-2/drop/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop/props.ma
-LambdaDelta-2/drop1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop1/defs.ma
-LambdaDelta-2/drop1/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop1/fwd.ma
-LambdaDelta-2/drop1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop1/props.ma
-LambdaDelta-2/drop1/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop1/getl.ma
-LambdaDelta-2/clear/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clear/defs.ma
-LambdaDelta-2/clear/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clear/fwd.ma
-LambdaDelta-2/clear/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clear/props.ma
-LambdaDelta-2/clear/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clear/drop.ma
-LambdaDelta-2/getl/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/defs.ma
-LambdaDelta-2/getl/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/fwd.ma
-LambdaDelta-2/getl/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/props.ma
-LambdaDelta-2/getl/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/clear.ma
-LambdaDelta-2/getl/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/drop.ma
-LambdaDelta-2/getl/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/getl.ma
-LambdaDelta-2/getl/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/dec.ma
-LambdaDelta-2/getl/flt.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/flt.ma
-LambdaDelta-2/cimp/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/cimp/defs.ma
-LambdaDelta-2/cimp/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/cimp/props.ma
-LambdaDelta-2/csubv/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/defs.ma
-LambdaDelta-2/csubv/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/props.ma
-LambdaDelta-2/csubv/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/drop.ma
-LambdaDelta-2/csubv/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/clear.ma
-LambdaDelta-2/csubv/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/getl.ma
-LambdaDelta-2/subst0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/defs.ma
-LambdaDelta-2/subst0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/fwd.ma
-LambdaDelta-2/subst0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/props.ma
-LambdaDelta-2/subst0/subst0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/subst0.ma
-LambdaDelta-2/subst0/tlt.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/tlt.ma
-LambdaDelta-2/subst0/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/dec.ma
-LambdaDelta-2/subst/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst/defs.ma
-LambdaDelta-2/subst/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst/fwd.ma
-LambdaDelta-2/subst/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst/props.ma
-LambdaDelta-2/subst1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst1/defs.ma
-LambdaDelta-2/subst1/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst1/fwd.ma
-LambdaDelta-2/subst1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst1/props.ma
-LambdaDelta-2/subst1/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst1/subst1.ma
-LambdaDelta-2/csubst0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/defs.ma
-LambdaDelta-2/csubst0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/fwd.ma
-LambdaDelta-2/csubst0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/props.ma
-LambdaDelta-2/csubst0/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/drop.ma
-LambdaDelta-2/csubst0/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/clear.ma
-LambdaDelta-2/csubst0/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/getl.ma
-LambdaDelta-2/csubst1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst1/defs.ma
-LambdaDelta-2/csubst1/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst1/fwd.ma
-LambdaDelta-2/csubst1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst1/props.ma
-LambdaDelta-2/csubst1/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst1/getl.ma
-LambdaDelta-2/fsubst0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/fsubst0/defs.ma
-LambdaDelta-2/fsubst0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/fsubst0/fwd.ma
-LambdaDelta-2/G/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/G/defs.ma
-LambdaDelta-2/next_plus/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/next_plus/defs.ma
-LambdaDelta-2/next_plus/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/next_plus/props.ma
-LambdaDelta-2/sty0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty0/defs.ma
-LambdaDelta-2/sty0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty0/fwd.ma
-LambdaDelta-2/sty0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty0/props.ma
-LambdaDelta-2/sty1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty1/defs.ma
-LambdaDelta-2/sty1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty1/props.ma
-LambdaDelta-2/sty1/cnt.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty1/cnt.ma
-LambdaDelta-2/A/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/A/defs.ma
-LambdaDelta-2/asucc/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/asucc/defs.ma
-LambdaDelta-2/asucc/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/asucc/fwd.ma
-LambdaDelta-2/aplus/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aplus/defs.ma
-LambdaDelta-2/aplus/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aplus/props.ma
-LambdaDelta-2/leq/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/leq/defs.ma
-LambdaDelta-2/leq/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/leq/fwd.ma
-LambdaDelta-2/leq/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/leq/props.ma
-LambdaDelta-2/leq/asucc.mma LambdaDelta-2/preamble.ma LambdaDelta-1/leq/asucc.ma
-LambdaDelta-2/llt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/llt/defs.ma
-LambdaDelta-2/llt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/llt/props.ma
-LambdaDelta-2/aprem/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aprem/defs.ma
-LambdaDelta-2/aprem/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aprem/fwd.ma
-LambdaDelta-2/aprem/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aprem/props.ma
-LambdaDelta-2/ex0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex0/defs.ma
-LambdaDelta-2/ex0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex0/props.ma
-LambdaDelta-2/arity/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/defs.ma
-LambdaDelta-2/arity/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/fwd.ma
-LambdaDelta-2/arity/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/props.ma
-LambdaDelta-2/arity/subst0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/subst0.ma
-LambdaDelta-2/arity/lift1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/lift1.ma
-LambdaDelta-2/arity/cimp.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/cimp.ma
-LambdaDelta-2/arity/aprem.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/aprem.ma
-LambdaDelta-2/pr0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/defs.ma
-LambdaDelta-2/pr0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/fwd.ma
-LambdaDelta-2/pr0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/props.ma
-LambdaDelta-2/pr0/pr0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/pr0.ma
-LambdaDelta-2/pr0/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/subst1.ma
-LambdaDelta-2/pr0/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/dec.ma
-LambdaDelta-2/pr1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr1/defs.ma
-LambdaDelta-2/pr1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr1/props.ma
-LambdaDelta-2/pr1/pr1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr1/pr1.ma
-LambdaDelta-2/wcpr0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wcpr0/defs.ma
-LambdaDelta-2/wcpr0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wcpr0/fwd.ma
-LambdaDelta-2/wcpr0/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wcpr0/getl.ma
-LambdaDelta-2/pr2/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/defs.ma
-LambdaDelta-2/pr2/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/fwd.ma
-LambdaDelta-2/pr2/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/props.ma
-LambdaDelta-2/pr2/clen.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/clen.ma
-LambdaDelta-2/pr2/pr2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/pr2.ma
-LambdaDelta-2/pr2/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/subst1.ma
-LambdaDelta-2/pr3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/defs.ma
-LambdaDelta-2/pr3/pr1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/pr1.ma
-LambdaDelta-2/pr3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/props.ma
-LambdaDelta-2/pr3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/fwd.ma
-LambdaDelta-2/pr3/wcpr0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/wcpr0.ma
-LambdaDelta-2/pr3/pr3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/pr3.ma
-LambdaDelta-2/pr3/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/subst1.ma
-LambdaDelta-2/pr3/iso.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/iso.ma
-LambdaDelta-2/csuba/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/defs.ma
-LambdaDelta-2/csuba/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/fwd.ma
-LambdaDelta-2/csuba/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/props.ma
-LambdaDelta-2/csuba/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/clear.ma
-LambdaDelta-2/csuba/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/drop.ma
-LambdaDelta-2/csuba/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/getl.ma
-LambdaDelta-2/csuba/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/arity.ma
-LambdaDelta-2/arity/pr3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/pr3.ma
-LambdaDelta-2/nf2/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/defs.ma
-LambdaDelta-2/nf2/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/fwd.ma
-LambdaDelta-2/nf2/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/props.ma
-LambdaDelta-2/nf2/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/arity.ma
-LambdaDelta-2/nf2/pr3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/pr3.ma
-LambdaDelta-2/nf2/lift1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/lift1.ma
-LambdaDelta-2/nf2/iso.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/iso.ma
-LambdaDelta-2/ex2/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex2/defs.ma
-LambdaDelta-2/ex2/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex2/props.ma
-LambdaDelta-2/nf2/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/dec.ma
-LambdaDelta-2/sn3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/defs.ma
-LambdaDelta-2/sn3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/fwd.ma
-LambdaDelta-2/sn3/nf2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/nf2.ma
-LambdaDelta-2/sn3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/props.ma
-LambdaDelta-2/sn3/lift1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/lift1.ma
-LambdaDelta-2/sc3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sc3/defs.ma
-LambdaDelta-2/sc3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sc3/props.ma
-LambdaDelta-2/csubc/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/defs.ma
-LambdaDelta-2/csubc/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/fwd.ma
-LambdaDelta-2/csubc/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/props.ma
-LambdaDelta-2/csubc/csuba.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/csuba.ma
-LambdaDelta-2/csubc/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/drop.ma
-LambdaDelta-2/csubc/drop1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/drop1.ma
-LambdaDelta-2/csubc/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/clear.ma
-LambdaDelta-2/csubc/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/getl.ma
-LambdaDelta-2/csubc/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/arity.ma
-LambdaDelta-2/sc3/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sc3/arity.ma
-LambdaDelta-2/pc1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc1/defs.ma
-LambdaDelta-2/pc1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc1/props.ma
-LambdaDelta-2/pc3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/defs.ma
-LambdaDelta-2/pc3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/props.ma
-LambdaDelta-2/pc3/pc1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/pc1.ma
-LambdaDelta-2/pc3/nf2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/nf2.ma
-LambdaDelta-2/pc3/wcpr0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/wcpr0.ma
-LambdaDelta-2/pc3/left.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/left.ma
-LambdaDelta-2/pc3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/fwd.ma
-LambdaDelta-2/pc3/fsubst0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/fsubst0.ma
-LambdaDelta-2/pc3/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/subst1.ma
-LambdaDelta-2/ty3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/defs.ma
-LambdaDelta-2/ty3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/fwd.ma
-LambdaDelta-2/ex1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex1/defs.ma
-LambdaDelta-2/ex1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex1/props.ma
-LambdaDelta-2/ty3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/props.ma
-LambdaDelta-2/ty3/fsubst0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/fsubst0.ma
-LambdaDelta-2/ty3/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/subst1.ma
-LambdaDelta-2/csubt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/defs.ma
-LambdaDelta-2/csubt/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/fwd.ma
-LambdaDelta-2/csubt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/props.ma
-LambdaDelta-2/csubt/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/clear.ma
-LambdaDelta-2/csubt/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/drop.ma
-LambdaDelta-2/csubt/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/getl.ma
-LambdaDelta-2/csubt/pc3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/pc3.ma
-LambdaDelta-2/csubt/ty3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/ty3.ma
-LambdaDelta-2/ty3/pr3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/pr3.ma
-LambdaDelta-2/ty3/pr3_props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/pr3_props.ma
-LambdaDelta-2/ty3/sty0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/sty0.ma
-LambdaDelta-2/ty3/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/arity.ma
-LambdaDelta-2/ty3/arity_props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/arity_props.ma
-LambdaDelta-2/csubt/csuba.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/csuba.ma
-LambdaDelta-2/ty3/fwd_nf2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/fwd_nf2.ma
-LambdaDelta-2/ty3/nf2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/nf2.ma
-LambdaDelta-2/pc3/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/dec.ma
-LambdaDelta-2/ty3/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/dec.ma
-LambdaDelta-2/wf3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/defs.ma
-LambdaDelta-2/wf3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/fwd.ma
-LambdaDelta-2/wf3/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/clear.ma
-LambdaDelta-2/wf3/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/getl.ma
-LambdaDelta-2/wf3/ty3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/ty3.ma
-LambdaDelta-2/wf3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/props.ma
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/.depend b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/.depend
deleted file mode 100644
index 925c30793..000000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/.depend
+++ /dev/null
@@ -1,2 +0,0 @@
-Legacy-2/coq/defs.ma: Legacy-2/coq/defs.mma Legacy-2/preamble.ma
-Legacy-2/coq/props.ma: Legacy-2/coq/props.mma Legacy-2/coq/defs.ma
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/depends b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/depends
deleted file mode 100644
index 0faac1049..000000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/depends
+++ /dev/null
@@ -1,2 +0,0 @@
-Legacy-2/coq/defs.mma Legacy-2/preamble.ma Legacy-1/coq/defs.ma
-Legacy-2/coq/props.mma Legacy-2/preamble.ma Legacy-1/coq/props.ma
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
index 194fc389e..28fe09079 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
@@ -1,68 +1,39 @@
 include ../Makefile.defs
 
+DIR=$(shell basename $$PWD)
+
 H=@
-S=-s
 
 MATITAOPTIONS=$(MATITAUSEROPTIONS) -onepass
 
 LOG = log.txt
 
-DIRS = Legacy-2 Base-2 LambdaDelta-2
-
-SILENTMAKE = $(H)$(MAKE) $(S) --no-print-directory H=$(H) S=$(S)
-
-MAS = $(shell find $(DIRS) -mindepth 2 -name "*.ma")
+DEVELS = Legacy-2 Base-2 LambdaDelta-2
 
-all: depends
-	$(H)$(RM) $(LOG)
-	$(SILENTMAKE) build
+MAS = $(shell find $(DEVELS) -mindepth 2 -name "*.ma")
 
-opt all.opt: depends
+$(DIR) all:
 	$(H)$(RM) $(LOG)
-	$(SILENTMAKE) build.opt
-
-%.build.opt:
-	$(SILENTMAKE) $(patsubst %.mma, %.ma, $(shell find $* -name "*.mma"))
-	$(H)echo $*/theory.ma `$(BIN)matitadep.opt -stdout $*/theory.ma` >> depends
-
-build: $(DIRS:%=%.build.opt)
 	$(H)$(BIN)matitac $(MATITAOPTIONS) 2>> $(LOG)
-	$(H)$(RM) depends
-
-build.opt: $(DIRS:%=%.build.opt)
+$(DIR).opt opt all.opt:
+	$(H)$(RM) $(LOG)
 	$(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2>> $(LOG)
-	$(H)$(RM) depends
-
 clean:
 	$(H)$(BIN)matitaclean $(MATITAOPTIONS)
-	$(H)rm -f $(MAS) depends
-
+	$(H)$(RM) $(MAS)
 clean.opt:
 	$(H)$(BIN)matitaclean.opt $(MATITAOPTIONS)
-	$(H)rm -f $(MAS) depends
-
-clean.ma:
-	$(H)$(BIN)matitaclean.opt $(MATITAOPTIONS) $(MAS)
-	$(H)$(RM) $(MAS) depends
-
-clean.mma:
-#	$(H)for FILE in */*.mma ; do if [ -e ../LambdaDelta-1/$${FILE/.mma/.ma} ] ; then true ; else rm $$FILE ; fi done
-
+	$(H)$(RM) $(MAS)
 depend:
-	@echo matitadep
-	$(H)$(BIN)matitadep $(foreach DIR, $(DIRS), -exclude $(DIR)/theory.ma)
-	$(H)cat $(DIRS:%=%/depends) >> depends
-
+	$$(H)(BIN)matitadep $(MATITAOPTIONS)
 depend.opt:
-	@echo matitadep.opt
-	$(H)$(BIN)matitadep.opt $(foreach DIR, $(DIRS), -exclude $(DIR)/theory.ma)
-	$(H)cat $(DIRS:%=%/depends) >> depends
+	$(H)$(BIN)matitadep.opt $(MATITAOPTIONS)
 
-depends: depend.opt
-
-%.ma: %.mma
-	$(H)$(BIN)matitac.opt $(MATITAOPTIONS) $(word 3,$(shell grep -h $< */depends)) `$(BIN)matitadep.opt -stdout $<` 2>> $(LOG)
-	$(H)$(BIN)matitac.opt $(MATITAOPTIONS) -dump $@ $< 2>> $(LOG)
-	$(H)echo $@ `$(BIN)matitadep.opt -stdout $@` >> depends
-
-$(foreach DIR, $(DIRS), $(eval include $(DIR)/.depend))
+ifneq ($(strip $(MAS)),)
+clean.ma:
+	$(H)$(BIN)matitaclean.opt $(MATITAOPTIONS) $(MAS)
+	$(H)$(RM) $(MAS)
+else
+clean.ma:
+	$(H)echo no files to clean
+endif
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/depends b/helm/software/matita/contribs/LAMBDA-TYPES/depends
new file mode 100644
index 000000000..cda04b715
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/depends
@@ -0,0 +1,696 @@
+LambdaDelta-2/csuba/fwd.mma LambdaDelta-1/csuba/fwd.ma LambdaDelta-2/csuba/defs.ma
+LambdaDelta-1/csubst1/props.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/subst1/defs.ma
+LambdaDelta-1/asucc/fwd.ma LambdaDelta-1/asucc/defs.ma
+LambdaDelta-2/ty3/dec.ma LambdaDelta-2/ty3/dec.mma
+Base-2/plist/defs.mma Base-2/preamble.ma
+LambdaDelta-1/leq/defs.ma LambdaDelta-1/aplus/defs.ma
+LambdaDelta-2/csuba/getl.mma LambdaDelta-1/csuba/getl.ma LambdaDelta-2/csuba/clear.ma LambdaDelta-2/csuba/drop.ma LambdaDelta-2/getl/clear.ma
+LambdaDelta-1/pc3/props.ma LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/pr3.ma
+LambdaDelta-2/sn3/fwd.mma LambdaDelta-1/sn3/fwd.ma LambdaDelta-2/pr3/props.ma LambdaDelta-2/sn3/defs.ma
+LambdaDelta-2/lift1/fwd.mma LambdaDelta-1/lift1/fwd.ma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/lift1/defs.ma
+Legacy-1/theory.ma Legacy-1/coq/props.ma
+LambdaDelta-2/drop1/defs.mma LambdaDelta-2/drop/defs.ma LambdaDelta-2/lift1/defs.ma
+LambdaDelta-2/cnt/props.ma LambdaDelta-2/cnt/props.mma
+LambdaDelta-2/nf2/fwd.ma LambdaDelta-2/nf2/fwd.mma
+LambdaDelta-2/csubst1/defs.ma LambdaDelta-2/csubst1/defs.mma
+LambdaDelta-2/ty3/pr3.ma LambdaDelta-2/ty3/pr3.mma
+LambdaDelta-1/csubst0/props.ma LambdaDelta-1/csubst0/defs.ma
+LambdaDelta-2/ty3/props.mma LambdaDelta-1/ty3/props.ma LambdaDelta-2/pc3/fwd.ma LambdaDelta-2/ty3/fwd.ma
+LambdaDelta-2/sc3/arity.ma LambdaDelta-2/sc3/arity.mma
+LambdaDelta-2/pr1/props.mma LambdaDelta-1/pr1/props.ma LambdaDelta-2/T/props.ma LambdaDelta-2/pr0/subst1.ma LambdaDelta-2/pr1/defs.ma LambdaDelta-2/subst1/props.ma
+LambdaDelta-1/iso/props.ma LambdaDelta-1/iso/fwd.ma
+LambdaDelta-1/lift/tlt.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/tlt/props.ma
+LambdaDelta-2/pc3/dec.ma LambdaDelta-2/pc3/dec.mma
+LambdaDelta-1/next_plus/props.ma LambdaDelta-1/next_plus/defs.ma
+LambdaDelta-2/csubt/pc3.ma LambdaDelta-2/csubt/pc3.mma
+LambdaDelta-1/C/props.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/T/props.ma
+LambdaDelta-2/pc3/pc1.mma LambdaDelta-1/pc3/pc1.ma LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/pr3/pr1.ma
+LambdaDelta-2/csubc/clear.ma LambdaDelta-2/csubc/clear.mma
+LambdaDelta-2/subst0/defs.ma LambdaDelta-2/subst0/defs.mma
+LambdaDelta-1/pr3/pr1.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr3/defs.ma
+LambdaDelta-2/clear/props.mma LambdaDelta-1/clear/props.ma LambdaDelta-2/clear/fwd.ma
+LambdaDelta-1/fsubst0/fwd.ma LambdaDelta-1/fsubst0/defs.ma
+LambdaDelta-2/ty3/pr3_props.ma LambdaDelta-2/ty3/pr3_props.mma
+LambdaDelta-1/ex0/defs.ma LambdaDelta-1/A/defs.ma LambdaDelta-1/G/defs.ma
+Legacy-1/coq/defs.ma Legacy-1/preamble.ma
+LambdaDelta-1/wf3/fwd.ma LambdaDelta-1/wf3/defs.ma
+LambdaDelta-2/subst0/fwd.ma LambdaDelta-2/subst0/fwd.mma
+LambdaDelta-2/pr3/iso.mma LambdaDelta-1/pr3/iso.ma LambdaDelta-2/iso/props.ma LambdaDelta-2/pr3/fwd.ma LambdaDelta-2/tlist/props.ma
+LambdaDelta-1/pc3/wcpr0.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/wcpr0/getl.ma
+LambdaDelta-2/getl/dec.ma LambdaDelta-2/getl/dec.mma
+LambdaDelta-2/pr0/subst1.mma LambdaDelta-1/pr0/subst1.ma LambdaDelta-2/pr0/props.ma LambdaDelta-2/subst1/defs.ma
+LambdaDelta-2/csubst0/getl.ma LambdaDelta-2/csubst0/getl.mma
+LambdaDelta-2/csubc/csuba.ma LambdaDelta-2/csubc/csuba.mma
+LambdaDelta-2/pr3/props.mma LambdaDelta-1/pr3/props.ma LambdaDelta-2/pr1/props.ma LambdaDelta-2/pr2/props.ma LambdaDelta-2/pr3/pr1.ma
+LambdaDelta-1/tlt/defs.ma LambdaDelta-1/T/defs.ma
+LambdaDelta-2/drop/fwd.mma LambdaDelta-1/drop/fwd.ma LambdaDelta-2/drop/defs.ma
+LambdaDelta-1/drop/props.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/r/props.ma
+LambdaDelta-1/pc1/props.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pr1/pr1.ma
+LambdaDelta-2/wf3/ty3.mma LambdaDelta-1/wf3/ty3.ma LambdaDelta-2/wf3/getl.ma
+LambdaDelta-2/T/dec.mma LambdaDelta-1/T/dec.ma LambdaDelta-2/T/defs.ma
+LambdaDelta-1/subst0/tlt.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/lift/tlt.ma LambdaDelta-1/subst0/defs.ma
+LambdaDelta-2/aprem/props.mma LambdaDelta-1/aprem/props.ma LambdaDelta-2/aprem/fwd.ma LambdaDelta-2/leq/defs.ma
+LambdaDelta-2/csubv/props.ma LambdaDelta-2/csubv/props.mma
+LambdaDelta-2/ty3/defs.mma LambdaDelta-2/G/defs.ma LambdaDelta-2/pc3/defs.ma
+LambdaDelta-2/sn3/lift1.ma LambdaDelta-2/sn3/lift1.mma
+LambdaDelta-1/sn3/fwd.ma LambdaDelta-1/pr3/props.ma LambdaDelta-1/sn3/defs.ma
+LambdaDelta-1/T/defs.ma LambdaDelta-1/preamble.ma
+LambdaDelta-1/asucc/defs.ma LambdaDelta-1/A/defs.ma LambdaDelta-1/G/defs.ma
+LambdaDelta-2/aplus/defs.ma LambdaDelta-2/aplus/defs.mma
+LambdaDelta-2/sc3/props.ma LambdaDelta-2/sc3/props.mma
+LambdaDelta-2/csuba/clear.ma LambdaDelta-2/csuba/clear.mma
+LambdaDelta-1/subst1/subst1.ma LambdaDelta-1/subst0/subst0.ma LambdaDelta-1/subst1/fwd.ma
+LambdaDelta-2/wcpr0/fwd.mma LambdaDelta-1/wcpr0/fwd.ma LambdaDelta-2/wcpr0/defs.ma
+LambdaDelta-1/cimp/props.ma LambdaDelta-1/cimp/defs.ma LambdaDelta-1/getl/getl.ma
+LambdaDelta-2/ty3/nf2.mma LambdaDelta-1/ty3/nf2.ma LambdaDelta-2/nf2/arity.ma LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/ty3/arity.ma
+LambdaDelta-2/subst1/props.mma LambdaDelta-1/subst1/props.ma LambdaDelta-2/subst0/props.ma LambdaDelta-2/subst1/defs.ma
+LambdaDelta-2/lift/tlt.mma LambdaDelta-1/lift/tlt.ma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/tlt/props.ma
+LambdaDelta-2/getl/drop.ma LambdaDelta-2/getl/drop.mma
+LambdaDelta-2/csubst0/props.mma LambdaDelta-1/csubst0/props.ma LambdaDelta-2/csubst0/defs.ma
+LambdaDelta-1/r/defs.ma LambdaDelta-1/T/defs.ma
+LambdaDelta-1/ty3/fwd.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/ty3/defs.ma
+LambdaDelta-2/nf2/dec.ma LambdaDelta-2/nf2/dec.mma
+LambdaDelta-2/lift/props.ma LambdaDelta-2/lift/props.mma
+LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/csubst0/defs.ma
+LambdaDelta-1/subst/props.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst/fwd.ma LambdaDelta-1/subst0/defs.ma
+Base-1/theory.ma Base-1/blt/props.ma Base-1/ext/arith.ma Base-1/ext/tactics.ma Base-1/plist/props.ma Base-1/types/props.ma
+LambdaDelta-1/A/defs.ma LambdaDelta-1/preamble.ma
+LambdaDelta-2/C/props.mma LambdaDelta-1/C/props.ma LambdaDelta-2/C/defs.ma LambdaDelta-2/T/props.ma
+LambdaDelta-2/cnt/props.mma LambdaDelta-1/cnt/props.ma LambdaDelta-2/cnt/defs.ma LambdaDelta-2/lift/fwd.ma
+LambdaDelta-2/csubt/fwd.ma LambdaDelta-2/csubt/fwd.mma
+LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/nf2/pr3.mma
+LambdaDelta-2/subst1/fwd.ma LambdaDelta-2/subst1/fwd.mma
+LambdaDelta-2/subst/defs.mma LambdaDelta-2/lift/defs.ma
+LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/pr3/fwd.ma
+LambdaDelta-2/csubt/props.ma LambdaDelta-2/csubt/props.mma
+LambdaDelta-2/pr2/pr2.ma LambdaDelta-2/pr2/pr2.mma
+LambdaDelta-2/pc3/subst1.mma LambdaDelta-1/pc3/subst1.ma LambdaDelta-2/pc3/props.ma LambdaDelta-2/pr3/subst1.ma
+LambdaDelta-1/csuba/fwd.ma LambdaDelta-1/csuba/defs.ma
+LambdaDelta-2/subst0/dec.ma LambdaDelta-2/subst0/dec.mma
+LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/csubst0/clear.ma LambdaDelta-1/csubst0/drop.ma LambdaDelta-1/getl/fwd.ma
+LambdaDelta-2/ty3/sty0.ma LambdaDelta-2/ty3/sty0.mma
+LambdaDelta-2/pc3/fsubst0.ma LambdaDelta-2/pc3/fsubst0.mma
+LambdaDelta-2/wf3/props.mma LambdaDelta-1/wf3/props.ma LambdaDelta-2/app/defs.ma LambdaDelta-2/wf3/ty3.ma
+LambdaDelta-2/flt/props.mma LambdaDelta-1/flt/props.ma LambdaDelta-2/C/props.ma LambdaDelta-2/flt/defs.ma
+LambdaDelta-2/llt/defs.mma LambdaDelta-2/A/defs.ma
+Legacy-1/definitions.ma Legacy-1/coq/defs.ma
+LambdaDelta-2/csubt/props.mma LambdaDelta-1/csubt/props.ma LambdaDelta-2/csubt/defs.ma
+LambdaDelta-1/sn3/props.ma LambdaDelta-1/nf2/iso.ma LambdaDelta-1/pr3/iso.ma LambdaDelta-1/sn3/fwd.ma LambdaDelta-1/sn3/nf2.ma
+LambdaDelta-2/clear/drop.ma LambdaDelta-2/clear/drop.mma
+LambdaDelta-1/drop1/defs.ma LambdaDelta-1/drop/defs.ma LambdaDelta-1/lift1/defs.ma
+LambdaDelta-2/ty3/fwd_nf2.ma LambdaDelta-2/ty3/fwd_nf2.mma
+LambdaDelta-1/pc3/left.ma LambdaDelta-1/pc3/props.ma
+LambdaDelta-2/pr3/iso.ma LambdaDelta-2/pr3/iso.mma
+LambdaDelta-2/csubt/defs.ma LambdaDelta-2/csubt/defs.mma
+LambdaDelta-2/pc3/pc1.ma LambdaDelta-2/pc3/pc1.mma
+LambdaDelta-1/definitions.ma LambdaDelta-1/app/defs.ma LambdaDelta-1/aprem/defs.ma LambdaDelta-1/cimp/defs.ma LambdaDelta-1/clen/defs.ma LambdaDelta-1/cnt/defs.ma LambdaDelta-1/csuba/defs.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/csubt/defs.ma LambdaDelta-1/csubv/defs.ma LambdaDelta-1/ex0/defs.ma LambdaDelta-1/ex1/defs.ma LambdaDelta-1/ex2/defs.ma LambdaDelta-1/flt/defs.ma LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/iso/defs.ma LambdaDelta-1/llt/defs.ma LambdaDelta-1/next_plus/defs.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/sty1/defs.ma LambdaDelta-1/subst/defs.ma LambdaDelta-1/subst1/defs.ma LambdaDelta-1/tlt/defs.ma LambdaDelta-1/wcpr0/defs.ma LambdaDelta-1/wf3/defs.ma
+LambdaDelta-1/getl/getl.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma
+LambdaDelta-2/arity/pr3.mma LambdaDelta-1/arity/pr3.ma LambdaDelta-2/arity/subst0.ma LambdaDelta-2/csuba/arity.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/pr1/defs.ma LambdaDelta-2/pr3/defs.ma LambdaDelta-2/wcpr0/getl.ma
+LambdaDelta-2/pc3/subst1.ma LambdaDelta-2/pc3/subst1.mma
+LambdaDelta-1/csubt/drop.ma LambdaDelta-1/csubt/fwd.ma LambdaDelta-1/drop/fwd.ma
+LambdaDelta-2/pr2/defs.ma LambdaDelta-2/pr2/defs.mma
+LambdaDelta-2/sty1/props.mma LambdaDelta-1/sty1/props.ma LambdaDelta-2/sty0/props.ma LambdaDelta-2/sty1/defs.ma
+LambdaDelta-2/pr3/defs.mma LambdaDelta-2/pr2/defs.ma
+LambdaDelta-2/csubv/props.mma LambdaDelta-1/csubv/props.ma LambdaDelta-2/T/props.ma LambdaDelta-2/csubv/defs.ma
+LambdaDelta-1/ty3/dec.ma LambdaDelta-1/getl/dec.ma LambdaDelta-1/getl/flt.ma LambdaDelta-1/pc3/dec.ma
+LambdaDelta-2/csuba/defs.ma LambdaDelta-2/csuba/defs.mma
+LambdaDelta-2/sty1/defs.ma LambdaDelta-2/sty1/defs.mma
+LambdaDelta-2/sn3/defs.ma LambdaDelta-2/sn3/defs.mma
+LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pc1/defs.mma
+LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst0/defs.ma
+Base-2/plist/props.ma Base-2/plist/props.mma
+LambdaDelta-1/csubv/defs.ma LambdaDelta-1/C/defs.ma
+LambdaDelta-1/csuba/drop.ma LambdaDelta-1/csuba/fwd.ma LambdaDelta-1/drop/fwd.ma
+Base-1/definitions.ma Base-1/blt/defs.ma Base-1/plist/defs.ma Base-1/types/defs.ma
+LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/T/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/clen.ma LambdaDelta-1/subst0/dec.ma
+LambdaDelta-1/leq/props.ma LambdaDelta-1/aplus/props.ma LambdaDelta-1/leq/fwd.ma
+LambdaDelta-1/ty3/pr3.ma LambdaDelta-1/csubt/ty3.ma LambdaDelta-1/pc1/props.ma LambdaDelta-1/pc3/pc1.ma LambdaDelta-1/pc3/wcpr0.ma LambdaDelta-1/ty3/fsubst0.ma LambdaDelta-1/ty3/subst1.ma
+LambdaDelta-2/lift1/defs.ma LambdaDelta-2/lift1/defs.mma
+LambdaDelta-2/aprem/fwd.mma LambdaDelta-1/aprem/fwd.ma LambdaDelta-2/aprem/defs.ma
+LambdaDelta-1/sty0/defs.ma LambdaDelta-1/G/defs.ma LambdaDelta-1/getl/defs.ma
+Base-2/ext/tactics.ma Base-2/ext/tactics.mma
+LambdaDelta-2/drop1/props.ma LambdaDelta-2/drop1/props.mma
+LambdaDelta-2/getl/fwd.mma LambdaDelta-1/getl/fwd.ma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/getl/defs.ma
+LambdaDelta-1/subst1/defs.ma LambdaDelta-1/subst0/defs.ma
+LambdaDelta-2/wcpr0/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/pr0/defs.ma
+LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr0/props.ma LambdaDelta-1/subst1/defs.ma
+LambdaDelta-2/ty3/pr3.mma LambdaDelta-1/ty3/pr3.ma LambdaDelta-2/csubt/ty3.ma LambdaDelta-2/pc1/props.ma LambdaDelta-2/pc3/pc1.ma LambdaDelta-2/pc3/wcpr0.ma LambdaDelta-2/ty3/fsubst0.ma LambdaDelta-2/ty3/subst1.ma
+LambdaDelta-2/drop/props.mma LambdaDelta-1/drop/props.ma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/lift/props.ma LambdaDelta-2/r/props.ma
+LambdaDelta-2/ty3/arity.ma LambdaDelta-2/ty3/arity.mma
+LambdaDelta-1/pc3/dec.ma LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/ty3/arity_props.ma
+LambdaDelta-2/csubst1/defs.mma LambdaDelta-2/csubst0/defs.ma
+LambdaDelta-2/pr2/defs.mma LambdaDelta-2/getl/defs.ma LambdaDelta-2/pr0/defs.ma
+LambdaDelta-2/csubst0/clear.mma LambdaDelta-1/csubst0/clear.ma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/csubst0/props.ma
+LambdaDelta-2/arity/fwd.mma LambdaDelta-1/arity/fwd.ma LambdaDelta-2/arity/defs.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/leq/asucc.ma
+Base-1/types/defs.ma Base-1/preamble.ma
+LambdaDelta-1/cimp/defs.ma LambdaDelta-1/getl/defs.ma
+LambdaDelta-2/leq/props.mma LambdaDelta-1/leq/props.ma LambdaDelta-2/aplus/props.ma LambdaDelta-2/leq/fwd.ma
+LambdaDelta-2/subst1/fwd.mma LambdaDelta-1/subst1/fwd.ma LambdaDelta-2/subst0/props.ma LambdaDelta-2/subst1/defs.ma
+LambdaDelta-2/T/dec.ma LambdaDelta-2/T/dec.mma
+LambdaDelta-2/nf2/pr3.mma LambdaDelta-1/nf2/pr3.ma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr3/pr3.ma
+LambdaDelta-2/sty1/cnt.mma LambdaDelta-1/sty1/cnt.ma LambdaDelta-2/cnt/props.ma LambdaDelta-2/sty1/props.ma
+LambdaDelta-2/pr3/pr1.mma LambdaDelta-1/pr3/pr1.ma LambdaDelta-2/pr1/defs.ma LambdaDelta-2/pr3/defs.ma
+LambdaDelta-1/lift/defs.ma LambdaDelta-1/s/defs.ma LambdaDelta-1/tlist/defs.ma
+LambdaDelta-1/cnt/defs.ma LambdaDelta-1/T/defs.ma
+LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/defs.ma
+LambdaDelta-1/subst0/subst0.ma LambdaDelta-1/subst0/props.ma
+LambdaDelta-2/arity/fwd.ma LambdaDelta-2/arity/fwd.mma
+LambdaDelta-2/app/defs.ma LambdaDelta-2/app/defs.mma
+LambdaDelta-2/T/defs.mma LambdaDelta-2/preamble.ma
+LambdaDelta-2/pr1/defs.mma LambdaDelta-2/pr0/defs.ma
+LambdaDelta-1/clen/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/s/defs.ma
+LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/pr0/fwd.mma
+Base-1/types/props.ma Base-1/types/defs.ma
+LambdaDelta-2/flt/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/leq/fwd.ma LambdaDelta-2/leq/fwd.mma
+LambdaDelta-1/pr2/subst1.ma LambdaDelta-1/csubst1/fwd.ma LambdaDelta-1/csubst1/getl.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr2/defs.ma LambdaDelta-1/subst1/subst1.ma
+LambdaDelta-2/ty3/fwd.mma LambdaDelta-1/ty3/fwd.ma LambdaDelta-2/pc3/props.ma LambdaDelta-2/ty3/defs.ma
+LambdaDelta-1/T/dec.ma LambdaDelta-1/T/defs.ma
+LambdaDelta-2/csuba/arity.mma LambdaDelta-1/csuba/arity.ma LambdaDelta-2/arity/props.ma LambdaDelta-2/csuba/getl.ma LambdaDelta-2/csuba/props.ma LambdaDelta-2/csubv/getl.ma
+LambdaDelta-2/csubst0/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-2/drop1/getl.ma LambdaDelta-2/drop1/getl.mma
+Base-2/types/defs.mma Base-2/preamble.ma
+LambdaDelta-2/subst1/subst1.mma LambdaDelta-1/subst1/subst1.ma LambdaDelta-2/subst0/subst0.ma LambdaDelta-2/subst1/fwd.ma
+LambdaDelta-2/clen/getl.ma LambdaDelta-2/clen/getl.mma
+LambdaDelta-2/fsubst0/fwd.ma LambdaDelta-2/fsubst0/fwd.mma
+LambdaDelta-2/drop/defs.ma LambdaDelta-2/drop/defs.mma
+LambdaDelta-2/pr0/fwd.mma LambdaDelta-1/pr0/fwd.ma LambdaDelta-2/pr0/props.ma
+LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr0/defs.ma
+LambdaDelta-1/getl/clear.ma LambdaDelta-1/clear/drop.ma LambdaDelta-1/getl/props.ma
+LambdaDelta-2/clear/fwd.mma LambdaDelta-1/clear/fwd.ma LambdaDelta-2/clear/defs.ma
+LambdaDelta-1/nf2/lift1.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/nf2/props.ma
+LambdaDelta-2/wf3/clear.mma LambdaDelta-1/wf3/clear.ma LambdaDelta-2/wf3/fwd.ma
+Base-2/types/props.mma Base-1/types/props.ma Base-2/types/defs.ma
+LambdaDelta-2/pr0/defs.mma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-1/csubst1/fwd.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/subst1/props.ma
+LambdaDelta-2/nf2/fwd.mma LambdaDelta-1/nf2/fwd.ma LambdaDelta-2/T/props.ma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/clen.ma LambdaDelta-2/subst0/dec.ma
+LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/drop1/defs.ma
+LambdaDelta-2/csubt/clear.mma LambdaDelta-1/csubt/clear.ma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/csubt/defs.ma
+LambdaDelta-2/ex0/props.mma LambdaDelta-1/ex0/props.ma LambdaDelta-2/aplus/props.ma LambdaDelta-2/ex0/defs.ma LambdaDelta-2/leq/defs.ma
+LambdaDelta-2/wf3/ty3.ma LambdaDelta-2/wf3/ty3.mma
+LambdaDelta-2/ty3/props.ma LambdaDelta-2/ty3/props.mma
+LambdaDelta-2/wf3/fwd.mma LambdaDelta-1/wf3/fwd.ma LambdaDelta-2/wf3/defs.ma
+LambdaDelta-2/getl/defs.mma LambdaDelta-2/clear/defs.ma LambdaDelta-2/drop/defs.ma
+LambdaDelta-2/csubc/arity.mma LambdaDelta-1/csubc/arity.ma LambdaDelta-2/csubc/csuba.ma
+LambdaDelta-2/wcpr0/defs.ma LambdaDelta-2/wcpr0/defs.mma
+Base-1/spare.ma Base-1/theory.ma
+LambdaDelta-1/csubc/fwd.ma LambdaDelta-1/csubc/defs.ma
+LambdaDelta-1/aprem/props.ma LambdaDelta-1/aprem/fwd.ma LambdaDelta-1/leq/defs.ma
+LambdaDelta-1/tlt/props.ma LambdaDelta-1/tlt/defs.ma
+LambdaDelta-1/nf2/dec.ma LambdaDelta-1/C/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr0/dec.ma LambdaDelta-1/pr2/clen.ma LambdaDelta-1/pr2/fwd.ma
+Legacy-2/preamble.ma Legacy-1/preamble.ma Legacy-1/coq/defs.ma Legacy-1/coq/props.ma Legacy-1/definitions.ma
+Base-2/blt/props.mma Base-1/blt/props.ma Base-2/blt/defs.ma
+LambdaDelta-1/csubc/arity.ma LambdaDelta-1/csubc/csuba.ma
+LambdaDelta-2/aprem/defs.mma LambdaDelta-2/A/defs.ma
+LambdaDelta-2/csubv/getl.ma LambdaDelta-2/csubv/getl.mma
+LambdaDelta-2/tlist/defs.ma LambdaDelta-2/tlist/defs.mma
+LambdaDelta-2/subst0/tlt.mma LambdaDelta-1/subst0/tlt.ma LambdaDelta-2/lift/props.ma LambdaDelta-2/lift/tlt.ma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-2/sn3/lift1.mma LambdaDelta-1/sn3/lift1.ma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/lift1/fwd.ma LambdaDelta-2/sn3/props.ma
+LambdaDelta-1/wf3/props.ma LambdaDelta-1/app/defs.ma LambdaDelta-1/wf3/ty3.ma
+LambdaDelta-2/sty0/fwd.ma LambdaDelta-2/sty0/fwd.mma
+LambdaDelta-2/subst/fwd.mma LambdaDelta-1/subst/fwd.ma LambdaDelta-2/subst/defs.ma
+LambdaDelta-2/csubv/clear.mma LambdaDelta-1/csubv/clear.ma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/csubv/defs.ma
+LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr3/pr3.ma
+LambdaDelta-1/sty1/cnt.ma LambdaDelta-1/cnt/props.ma LambdaDelta-1/sty1/props.ma
+LambdaDelta-2/pr0/pr0.ma LambdaDelta-2/pr0/pr0.mma
+LambdaDelta-1/wf3/getl.ma LambdaDelta-1/ty3/dec.ma LambdaDelta-1/wf3/clear.ma
+LambdaDelta-2/ex2/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/ex2/props.mma LambdaDelta-1/ex2/props.ma LambdaDelta-2/arity/fwd.ma LambdaDelta-2/ex2/defs.ma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/fwd.ma
+LambdaDelta-2/iso/fwd.ma LambdaDelta-2/iso/fwd.mma
+LambdaDelta-2/subst/props.ma LambdaDelta-2/subst/props.mma
+LambdaDelta-2/wf3/getl.mma LambdaDelta-1/wf3/getl.ma LambdaDelta-2/ty3/dec.ma LambdaDelta-2/wf3/clear.ma
+LambdaDelta-1/pr2/pr2.ma LambdaDelta-1/getl/props.ma LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/pr2/defs.ma
+LambdaDelta-2/app/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-1/G/defs.ma LambdaDelta-1/preamble.ma
+Legacy-2/coq/defs.mma Legacy-2/preamble.ma
+LambdaDelta-2/csubv/drop.mma LambdaDelta-1/csubv/drop.ma LambdaDelta-2/csubv/props.ma LambdaDelta-2/drop/fwd.ma
+LambdaDelta-2/pr3/pr3.mma LambdaDelta-1/pr3/pr3.ma LambdaDelta-2/pr2/pr2.ma LambdaDelta-2/pr3/props.ma
+LambdaDelta-1/theory.ma LambdaDelta-1/csubt/csuba.ma LambdaDelta-1/ex0/props.ma LambdaDelta-1/ex1/props.ma LambdaDelta-1/ex2/props.ma LambdaDelta-1/pr3/wcpr0.ma LambdaDelta-1/sty1/cnt.ma LambdaDelta-1/subst/props.ma LambdaDelta-1/subst0/tlt.ma LambdaDelta-1/ty3/fwd_nf2.ma LambdaDelta-1/ty3/nf2.ma LambdaDelta-1/ty3/sty0.ma LambdaDelta-1/wcpr0/fwd.ma LambdaDelta-1/wf3/props.ma
+LambdaDelta-1/lift/fwd.ma LambdaDelta-1/lift/defs.ma
+LambdaDelta-2/arity/subst0.mma LambdaDelta-1/arity/subst0.ma LambdaDelta-2/arity/props.ma LambdaDelta-2/csubst0/getl.ma LambdaDelta-2/fsubst0/fwd.ma LambdaDelta-2/getl/getl.ma LambdaDelta-2/subst0/dec.ma LambdaDelta-2/subst0/fwd.ma
+LambdaDelta-2/wcpr0/fwd.ma LambdaDelta-2/wcpr0/fwd.mma
+LambdaDelta-2/pr0/dec.ma LambdaDelta-2/pr0/dec.mma
+LambdaDelta-2/csubc/getl.ma LambdaDelta-2/csubc/getl.mma
+LambdaDelta-1/arity/aprem.ma LambdaDelta-1/aprem/props.ma LambdaDelta-1/arity/cimp.ma LambdaDelta-1/arity/props.ma
+LambdaDelta-2/ex1/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/next_plus/defs.mma LambdaDelta-2/G/defs.ma
+LambdaDelta-2/arity/pr3.ma LambdaDelta-2/arity/pr3.mma
+LambdaDelta-2/csuba/props.mma LambdaDelta-1/csuba/props.ma LambdaDelta-2/csuba/defs.ma
+LambdaDelta-2/preamble.ma Base-2/theory.ma LambdaDelta-1/definitions.ma
+LambdaDelta-1/csuba/arity.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/csuba/getl.ma LambdaDelta-1/csuba/props.ma LambdaDelta-1/csubv/getl.ma
+LambdaDelta-2/ex2/defs.ma LambdaDelta-2/ex2/defs.mma
+Base-2/ext/arith.ma Base-2/ext/arith.mma
+LambdaDelta-1/pr3/iso.ma LambdaDelta-1/iso/props.ma LambdaDelta-1/pr3/fwd.ma LambdaDelta-1/tlist/props.ma
+LambdaDelta-1/csubv/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubv/defs.ma
+LambdaDelta-2/sty1/defs.mma LambdaDelta-2/sty0/defs.ma
+LambdaDelta-2/llt/props.ma LambdaDelta-2/llt/props.mma
+LambdaDelta-1/csubc/props.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/props.ma
+LambdaDelta-1/pc3/pc1.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/pr1.ma
+LambdaDelta-2/csubst0/drop.ma LambdaDelta-2/csubst0/drop.mma
+LambdaDelta-2/C/defs.ma LambdaDelta-2/C/defs.mma
+LambdaDelta-2/csubc/defs.mma LambdaDelta-2/sc3/defs.ma
+LambdaDelta-2/ex0/defs.mma LambdaDelta-2/A/defs.ma LambdaDelta-2/G/defs.ma
+LambdaDelta-1/subst/fwd.ma LambdaDelta-1/subst/defs.ma
+LambdaDelta-2/sc3/arity.mma LambdaDelta-1/sc3/arity.ma LambdaDelta-2/csubc/arity.ma LambdaDelta-2/csubc/drop1.ma LambdaDelta-2/csubc/getl.ma LambdaDelta-2/csubc/props.ma
+LambdaDelta-2/pr3/fwd.mma LambdaDelta-1/pr3/fwd.ma LambdaDelta-2/pr2/fwd.ma LambdaDelta-2/pr3/props.ma
+LambdaDelta-1/subst0/fwd.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst0/defs.ma
+LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/defs.ma
+LambdaDelta-2/sn3/nf2.ma LambdaDelta-2/sn3/nf2.mma
+LambdaDelta-2/csubt/pc3.mma LambdaDelta-1/csubt/pc3.ma LambdaDelta-2/csubt/getl.ma LambdaDelta-2/pc3/left.ma
+LambdaDelta-2/csubc/props.mma LambdaDelta-1/csubc/props.ma LambdaDelta-2/csubc/defs.ma LambdaDelta-2/sc3/props.ma
+LambdaDelta-2/csubt/drop.mma LambdaDelta-1/csubt/drop.ma LambdaDelta-2/csubt/fwd.ma LambdaDelta-2/drop/fwd.ma
+LambdaDelta-1/iso/defs.ma LambdaDelta-1/T/defs.ma
+LambdaDelta-2/sty0/defs.mma LambdaDelta-2/G/defs.ma LambdaDelta-2/getl/defs.ma
+LambdaDelta-2/pr2/fwd.ma LambdaDelta-2/pr2/fwd.mma
+LambdaDelta-2/nf2/defs.mma LambdaDelta-2/pr2/defs.ma
+LambdaDelta-2/leq/fwd.mma LambdaDelta-1/leq/fwd.ma LambdaDelta-2/leq/defs.ma
+LambdaDelta-2/ty3/nf2.ma LambdaDelta-2/ty3/nf2.mma
+LambdaDelta-2/pr3/props.ma LambdaDelta-2/pr3/props.mma
+LambdaDelta-2/flt/defs.ma LambdaDelta-2/flt/defs.mma
+LambdaDelta-2/getl/defs.ma LambdaDelta-2/getl/defs.mma
+LambdaDelta-2/aprem/defs.ma LambdaDelta-2/aprem/defs.mma
+LambdaDelta-2/wf3/clear.ma LambdaDelta-2/wf3/clear.mma
+LambdaDelta-1/aplus/defs.ma LambdaDelta-1/asucc/defs.ma
+LambdaDelta-2/clear/fwd.ma LambdaDelta-2/clear/fwd.mma
+LambdaDelta-1/cnt/props.ma LambdaDelta-1/cnt/defs.ma LambdaDelta-1/lift/fwd.ma
+LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/csubst0/fwd.mma
+LambdaDelta-2/r/props.mma LambdaDelta-1/r/props.ma LambdaDelta-2/r/defs.ma LambdaDelta-2/s/defs.ma
+LambdaDelta-2/pc3/dec.mma LambdaDelta-1/pc3/dec.ma LambdaDelta-2/nf2/fwd.ma LambdaDelta-2/ty3/arity_props.ma
+LambdaDelta-1/csubt/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubt/defs.ma
+LambdaDelta-2/pr2/pr2.mma LambdaDelta-1/pr2/pr2.ma LambdaDelta-2/getl/props.ma LambdaDelta-2/pr0/pr0.ma LambdaDelta-2/pr2/defs.ma
+LambdaDelta-2/pr2/props.ma LambdaDelta-2/pr2/props.mma
+LambdaDelta-1/csuba/props.ma LambdaDelta-1/csuba/defs.ma
+LambdaDelta-2/arity/defs.ma LambdaDelta-2/arity/defs.mma
+LambdaDelta-2/leq/asucc.ma LambdaDelta-2/leq/asucc.mma
+LambdaDelta-1/getl/fwd.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/getl/defs.ma
+LambdaDelta-2/subst1/defs.ma LambdaDelta-2/subst1/defs.mma
+LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/pc3/nf2.mma
+LambdaDelta-2/csuba/defs.mma LambdaDelta-2/arity/defs.ma
+LambdaDelta-1/lift/props.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/s/props.ma
+Base-2/blt/defs.mma Base-2/preamble.ma
+LambdaDelta-2/csubst1/props.ma LambdaDelta-2/csubst1/props.mma
+LambdaDelta-2/csubst1/getl.ma LambdaDelta-2/csubst1/getl.mma
+LambdaDelta-1/csubt/pc3.ma LambdaDelta-1/csubt/getl.ma LambdaDelta-1/pc3/left.ma
+LambdaDelta-1/ex1/defs.ma LambdaDelta-1/C/defs.ma
+LambdaDelta-2/pr3/wcpr0.ma LambdaDelta-2/pr3/wcpr0.mma
+LambdaDelta-1/sc3/arity.ma LambdaDelta-1/csubc/arity.ma LambdaDelta-1/csubc/drop1.ma LambdaDelta-1/csubc/getl.ma LambdaDelta-1/csubc/props.ma
+LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr0/props.ma
+LambdaDelta-2/T/props.ma LambdaDelta-2/T/props.mma
+LambdaDelta-1/leq/fwd.ma LambdaDelta-1/leq/defs.ma
+LambdaDelta-1/csubt/csuba.ma LambdaDelta-1/ty3/arity.ma
+Base-2/ext/arith.mma Base-1/ext/arith.ma Base-2/preamble.ma
+LambdaDelta-2/ty3/subst1.ma LambdaDelta-2/ty3/subst1.mma
+LambdaDelta-2/ty3/defs.ma LambdaDelta-2/ty3/defs.mma
+LambdaDelta-2/pr2/clen.mma LambdaDelta-1/pr2/clen.ma LambdaDelta-2/clen/getl.ma LambdaDelta-2/pr2/props.ma
+LambdaDelta-2/pc3/defs.mma LambdaDelta-2/pr3/defs.ma
+LambdaDelta-2/nf2/lift1.mma LambdaDelta-1/nf2/lift1.ma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/nf2/props.ma
+LambdaDelta-1/clear/props.ma LambdaDelta-1/clear/fwd.ma
+LambdaDelta-2/csubst0/props.ma LambdaDelta-2/csubst0/props.mma
+LambdaDelta-1/tlist/props.ma LambdaDelta-1/tlist/defs.ma
+LambdaDelta-2/pr1/props.ma LambdaDelta-2/pr1/props.mma
+Base-2/plist/defs.ma Base-2/plist/defs.mma
+LambdaDelta-1/subst1/fwd.ma LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst1/defs.ma
+LambdaDelta-2/tlist/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/flt/props.ma LambdaDelta-2/flt/props.mma
+LambdaDelta-2/s/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/pr0/defs.ma LambdaDelta-2/pr0/defs.mma
+LambdaDelta-2/nf2/defs.ma LambdaDelta-2/nf2/defs.mma
+Base-2/types/props.ma Base-2/types/props.mma
+LambdaDelta-1/csubst0/drop.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/s/props.ma
+LambdaDelta-2/pr3/fwd.ma LambdaDelta-2/pr3/fwd.mma
+LambdaDelta-2/iso/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/clear/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-1/subst0/dec.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst0/defs.ma
+LambdaDelta-2/clear/defs.ma LambdaDelta-2/clear/defs.mma
+LambdaDelta-2/csuba/clear.mma LambdaDelta-1/csuba/clear.ma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/csuba/defs.ma
+LambdaDelta-2/sc3/props.mma LambdaDelta-1/sc3/props.ma LambdaDelta-2/arity/aprem.ma LambdaDelta-2/arity/lift1.ma LambdaDelta-2/csuba/arity.ma LambdaDelta-2/drop1/getl.ma LambdaDelta-2/drop1/props.ma LambdaDelta-2/lift1/props.ma LambdaDelta-2/llt/props.ma LambdaDelta-2/nf2/lift1.ma LambdaDelta-2/sc3/defs.ma LambdaDelta-2/sn3/lift1.ma
+LambdaDelta-2/pr0/props.ma LambdaDelta-2/pr0/props.mma
+LambdaDelta-2/pr3/subst1.ma LambdaDelta-2/pr3/subst1.mma
+LambdaDelta-2/pr2/clen.ma LambdaDelta-2/pr2/clen.mma
+LambdaDelta-1/wf3/ty3.ma LambdaDelta-1/wf3/getl.ma
+LambdaDelta-2/sn3/props.mma LambdaDelta-1/sn3/props.ma LambdaDelta-2/nf2/iso.ma LambdaDelta-2/pr3/iso.ma LambdaDelta-2/sn3/fwd.ma LambdaDelta-2/sn3/nf2.ma
+LambdaDelta-1/sn3/lift1.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/lift1/fwd.ma LambdaDelta-1/sn3/props.ma
+LambdaDelta-2/wf3/defs.ma LambdaDelta-2/wf3/defs.mma
+LambdaDelta-1/s/defs.ma LambdaDelta-1/T/defs.ma
+LambdaDelta-1/sc3/props.ma LambdaDelta-1/arity/aprem.ma LambdaDelta-1/arity/lift1.ma LambdaDelta-1/csuba/arity.ma LambdaDelta-1/drop1/getl.ma LambdaDelta-1/drop1/props.ma LambdaDelta-1/lift1/props.ma LambdaDelta-1/llt/props.ma LambdaDelta-1/nf2/lift1.ma LambdaDelta-1/sc3/defs.ma LambdaDelta-1/sn3/lift1.ma
+LambdaDelta-1/csubt/defs.ma LambdaDelta-1/ty3/defs.ma
+LambdaDelta-1/arity/props.ma LambdaDelta-1/arity/fwd.ma
+LambdaDelta-1/clear/drop.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/drop/fwd.ma
+LambdaDelta-2/r/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/csubst0/fwd.mma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-2/csubst0/defs.ma
+LambdaDelta-2/csubst1/fwd.ma LambdaDelta-2/csubst1/fwd.mma
+LambdaDelta-2/getl/flt.ma LambdaDelta-2/getl/flt.mma
+LambdaDelta-2/csubv/getl.mma LambdaDelta-1/csubv/getl.ma LambdaDelta-2/csubv/clear.ma LambdaDelta-2/csubv/drop.ma LambdaDelta-2/getl/fwd.ma
+LambdaDelta-1/pc3/subst1.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/pr3/subst1.ma
+LambdaDelta-2/getl/props.ma LambdaDelta-2/getl/props.mma
+LambdaDelta-2/sc3/defs.ma LambdaDelta-2/sc3/defs.mma
+LambdaDelta-1/getl/drop.ma LambdaDelta-1/clear/drop.ma LambdaDelta-1/getl/props.ma
+Legacy-2/coq/props.mma Legacy-1/coq/props.ma Legacy-2/coq/defs.ma
+LambdaDelta-2/ty3/sty0.mma LambdaDelta-1/ty3/sty0.ma LambdaDelta-2/sty0/fwd.ma LambdaDelta-2/ty3/pr3_props.ma
+LambdaDelta-2/pc1/defs.mma LambdaDelta-2/pr1/defs.ma
+LambdaDelta-1/aplus/props.ma LambdaDelta-1/aplus/defs.ma LambdaDelta-1/next_plus/props.ma
+LambdaDelta-2/csubc/clear.mma LambdaDelta-1/csubc/clear.ma LambdaDelta-2/csubc/fwd.ma
+LambdaDelta-2/llt/defs.ma LambdaDelta-2/llt/defs.mma
+LambdaDelta-2/pr1/pr1.mma LambdaDelta-1/pr1/pr1.ma LambdaDelta-2/pr0/pr0.ma LambdaDelta-2/pr1/props.ma
+LambdaDelta-2/lift1/fwd.ma LambdaDelta-2/lift1/fwd.mma
+LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/lift/tlt.ma LambdaDelta-1/pr0/fwd.ma
+LambdaDelta-2/aprem/props.ma LambdaDelta-2/aprem/props.mma
+LambdaDelta-2/arity/defs.mma LambdaDelta-2/getl/defs.ma LambdaDelta-2/leq/defs.ma
+LambdaDelta-2/subst/defs.ma LambdaDelta-2/subst/defs.mma
+LambdaDelta-1/iso/fwd.ma LambdaDelta-1/iso/defs.ma LambdaDelta-1/tlist/defs.ma
+LambdaDelta-1/csuba/defs.ma LambdaDelta-1/arity/defs.ma
+LambdaDelta-2/aplus/defs.mma LambdaDelta-2/asucc/defs.ma
+LambdaDelta-1/ty3/arity_props.ma LambdaDelta-1/sc3/arity.ma LambdaDelta-1/ty3/arity.ma
+LambdaDelta-2/pc3/wcpr0.mma LambdaDelta-1/pc3/wcpr0.ma LambdaDelta-2/pc3/props.ma LambdaDelta-2/wcpr0/getl.ma
+LambdaDelta-2/csubc/arity.ma LambdaDelta-2/csubc/arity.mma
+LambdaDelta-1/getl/dec.ma LambdaDelta-1/getl/props.ma
+LambdaDelta-2/ex2/props.ma LambdaDelta-2/ex2/props.mma
+LambdaDelta-2/subst1/subst1.ma LambdaDelta-2/subst1/subst1.mma
+LambdaDelta-2/llt/props.mma LambdaDelta-1/llt/props.ma LambdaDelta-2/leq/defs.ma LambdaDelta-2/llt/defs.ma
+LambdaDelta-1/csubt/fwd.ma LambdaDelta-1/csubt/defs.ma
+LambdaDelta-1/csubst0/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst0/props.ma
+Legacy-2/coq/props.ma Legacy-2/coq/props.mma
+LambdaDelta-1/csubst1/getl.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/csubst1/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/subst1/props.ma
+Base-2/blt/defs.ma Base-2/blt/defs.mma
+LambdaDelta-1/pr0/dec.ma LambdaDelta-1/T/dec.ma LambdaDelta-1/T/props.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/subst0/dec.ma
+LambdaDelta-1/lift1/defs.ma LambdaDelta-1/lift/defs.ma
+LambdaDelta-2/subst0/dec.mma LambdaDelta-1/subst0/dec.ma LambdaDelta-2/lift/props.ma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-2/pr3/subst1.mma LambdaDelta-1/pr3/subst1.ma LambdaDelta-2/pr2/subst1.ma LambdaDelta-2/pr3/defs.ma
+LambdaDelta-2/pr0/props.mma LambdaDelta-1/pr0/props.ma LambdaDelta-2/pr0/defs.ma LambdaDelta-2/subst0/subst0.ma
+LambdaDelta-2/nf2/arity.ma LambdaDelta-2/nf2/arity.mma
+LambdaDelta-2/nf2/arity.mma LambdaDelta-1/nf2/arity.ma LambdaDelta-2/arity/subst0.ma LambdaDelta-2/nf2/fwd.ma
+Base-2/preamble.ma Base-1/definitions.ma Legacy-2/theory.ma
+LambdaDelta-2/csubt/getl.mma LambdaDelta-1/csubt/getl.ma LambdaDelta-2/csubt/clear.ma LambdaDelta-2/csubt/drop.ma LambdaDelta-2/getl/clear.ma
+LambdaDelta-2/ex1/props.ma LambdaDelta-2/ex1/props.mma
+LambdaDelta-2/csubt/ty3.ma LambdaDelta-2/csubt/ty3.mma
+LambdaDelta-2/next_plus/props.ma LambdaDelta-2/next_plus/props.mma
+LambdaDelta-2/arity/aprem.ma LambdaDelta-2/arity/aprem.mma
+Legacy-2/theory.ma Legacy-2/coq/props.ma
+LambdaDelta-2/drop/fwd.ma LambdaDelta-2/drop/fwd.mma
+LambdaDelta-2/pr2/props.mma LambdaDelta-1/pr2/props.ma LambdaDelta-2/getl/clear.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/pr0/props.ma LambdaDelta-2/pr2/defs.ma
+LambdaDelta-1/sn3/nf2.ma LambdaDelta-1/nf2/dec.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/sn3/defs.ma
+LambdaDelta-2/csuba/arity.ma LambdaDelta-2/csuba/arity.mma
+LambdaDelta-2/ex0/props.ma LambdaDelta-2/ex0/props.mma
+Base-2/plist/props.mma Base-1/plist/props.ma Base-2/plist/defs.ma
+LambdaDelta-2/sty1/props.ma LambdaDelta-2/sty1/props.mma
+LambdaDelta-2/pr3/pr3.ma LambdaDelta-2/pr3/pr3.mma
+LambdaDelta-2/pr3/defs.ma LambdaDelta-2/pr3/defs.mma
+LambdaDelta-2/csubv/clear.ma LambdaDelta-2/csubv/clear.mma
+LambdaDelta-2/fsubst0/fwd.mma LambdaDelta-1/fsubst0/fwd.ma LambdaDelta-2/fsubst0/defs.ma
+LambdaDelta-1/pr2/fwd.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr2/defs.ma
+LambdaDelta-2/pc3/left.mma LambdaDelta-1/pc3/left.ma LambdaDelta-2/pc3/props.ma
+LambdaDelta-2/csubc/props.ma LambdaDelta-2/csubc/props.mma
+LambdaDelta-1/drop1/getl.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/getl/drop.ma
+LambdaDelta-2/pc3/fsubst0.mma LambdaDelta-1/pc3/fsubst0.ma LambdaDelta-2/csubst0/getl.ma LambdaDelta-2/fsubst0/defs.ma LambdaDelta-2/pc3/left.ma
+LambdaDelta-2/G/defs.mma LambdaDelta-2/preamble.ma
+LambdaDelta-2/nf2/props.ma LambdaDelta-2/nf2/props.mma
+LambdaDelta-2/leq/defs.ma LambdaDelta-2/leq/defs.mma
+LambdaDelta-2/leq/asucc.mma LambdaDelta-1/leq/asucc.ma LambdaDelta-2/leq/props.ma
+LambdaDelta-2/drop/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/lift/defs.ma LambdaDelta-2/r/defs.ma
+LambdaDelta-1/ty3/nf2.ma LambdaDelta-1/nf2/arity.ma LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/ty3/arity.ma
+LambdaDelta-2/clen/getl.mma LambdaDelta-1/clen/getl.ma LambdaDelta-2/clen/defs.ma LambdaDelta-2/getl/props.ma
+LambdaDelta-2/csubt/getl.ma LambdaDelta-2/csubt/getl.mma
+LambdaDelta-2/sty0/props.ma LambdaDelta-2/sty0/props.mma
+LambdaDelta-2/ty3/arity_props.mma LambdaDelta-1/ty3/arity_props.ma LambdaDelta-2/sc3/arity.ma LambdaDelta-2/ty3/arity.ma
+LambdaDelta-2/sn3/defs.mma LambdaDelta-2/pr3/defs.ma
+LambdaDelta-1/sty1/defs.ma LambdaDelta-1/sty0/defs.ma
+LambdaDelta-2/subst0/props.mma LambdaDelta-1/subst0/props.ma LambdaDelta-2/subst0/fwd.ma
+LambdaDelta-2/pr0/pr0.mma LambdaDelta-1/pr0/pr0.ma LambdaDelta-2/lift/tlt.ma LambdaDelta-2/pr0/fwd.ma
+LambdaDelta-2/pc3/nf2.mma LambdaDelta-1/pc3/nf2.ma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/pc3/defs.ma
+LambdaDelta-1/ty3/sty0.ma LambdaDelta-1/sty0/fwd.ma LambdaDelta-1/ty3/pr3_props.ma
+LambdaDelta-2/csuba/getl.ma LambdaDelta-2/csuba/getl.mma
+LambdaDelta-1/lift1/props.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/lift/props.ma
+LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/pc3/defs.ma
+LambdaDelta-1/wcpr0/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/pr0/defs.ma
+LambdaDelta-2/asucc/fwd.mma LambdaDelta-1/asucc/fwd.ma LambdaDelta-2/asucc/defs.ma
+LambdaDelta-2/nf2/props.mma LambdaDelta-1/nf2/props.ma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/fwd.ma
+LambdaDelta-2/T/defs.ma LambdaDelta-2/T/defs.mma
+LambdaDelta-2/lift/tlt.ma LambdaDelta-2/lift/tlt.mma
+LambdaDelta-1/tlist/defs.ma LambdaDelta-1/T/defs.ma
+Base-2/blt/props.ma Base-2/blt/props.mma
+LambdaDelta-2/arity/cimp.mma LambdaDelta-1/arity/cimp.ma LambdaDelta-2/arity/defs.ma LambdaDelta-2/cimp/props.ma
+LambdaDelta-2/csubv/drop.ma LambdaDelta-2/csubv/drop.mma
+LambdaDelta-1/T/props.ma LambdaDelta-1/T/defs.ma
+LambdaDelta-2/arity/lift1.mma LambdaDelta-1/arity/lift1.ma LambdaDelta-2/arity/props.ma LambdaDelta-2/drop1/fwd.ma
+LambdaDelta-2/ex0/defs.ma LambdaDelta-2/ex0/defs.mma
+LambdaDelta-2/cimp/defs.mma LambdaDelta-2/getl/defs.ma
+LambdaDelta-2/drop1/getl.mma LambdaDelta-1/drop1/getl.ma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/getl/drop.ma
+Legacy-2/coq/defs.ma Legacy-2/coq/defs.mma
+LambdaDelta-2/aprem/fwd.ma LambdaDelta-2/aprem/fwd.mma
+LambdaDelta-2/subst1/defs.mma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-2/lift1/defs.mma LambdaDelta-2/lift/defs.ma
+LambdaDelta-1/csubv/getl.ma LambdaDelta-1/csubv/clear.ma LambdaDelta-1/csubv/drop.ma LambdaDelta-1/getl/fwd.ma
+LambdaDelta-2/csubt/clear.ma LambdaDelta-2/csubt/clear.mma
+LambdaDelta-1/ty3/arity.ma LambdaDelta-1/arity/pr3.ma LambdaDelta-1/asucc/fwd.ma LambdaDelta-1/ty3/pr3_props.ma
+LambdaDelta-2/csuba/props.ma LambdaDelta-2/csuba/props.mma
+LambdaDelta-2/next_plus/defs.ma LambdaDelta-2/next_plus/defs.mma
+LambdaDelta-1/arity/fwd.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/leq/asucc.ma
+LambdaDelta-2/r/defs.ma LambdaDelta-2/r/defs.mma
+LambdaDelta-2/csubst1/props.mma LambdaDelta-1/csubst1/props.ma LambdaDelta-2/csubst1/defs.ma LambdaDelta-2/subst1/defs.ma
+LambdaDelta-2/leq/defs.mma LambdaDelta-2/aplus/defs.ma
+LambdaDelta-2/asucc/fwd.ma LambdaDelta-2/asucc/fwd.mma
+LambdaDelta-2/tlt/defs.ma LambdaDelta-2/tlt/defs.mma
+LambdaDelta-2/arity/cimp.ma LambdaDelta-2/arity/cimp.mma
+LambdaDelta-1/pr2/defs.ma LambdaDelta-1/getl/defs.ma LambdaDelta-1/pr0/defs.ma
+Base-2/theory.ma Base-2/blt/props.ma Base-2/ext/arith.ma Base-2/ext/tactics.ma Base-2/plist/props.ma Base-2/types/props.ma
+LambdaDelta-1/csubc/getl.ma LambdaDelta-1/csubc/clear.ma LambdaDelta-1/csubc/drop.ma
+LambdaDelta-2/A/defs.ma LambdaDelta-2/A/defs.mma
+LambdaDelta-2/csubt/csuba.ma LambdaDelta-2/csubt/csuba.mma
+LambdaDelta-1/pr3/fwd.ma LambdaDelta-1/pr2/fwd.ma LambdaDelta-1/pr3/props.ma
+LambdaDelta-2/pc3/props.ma LambdaDelta-2/pc3/props.mma
+LambdaDelta-2/sty0/fwd.mma LambdaDelta-1/sty0/fwd.ma LambdaDelta-2/sty0/defs.ma
+LambdaDelta-2/csubc/drop.ma LambdaDelta-2/csubc/drop.mma
+LambdaDelta-1/clen/getl.ma LambdaDelta-1/clen/defs.ma LambdaDelta-1/getl/props.ma
+LambdaDelta-1/sn3/defs.ma LambdaDelta-1/pr3/defs.ma
+LambdaDelta-1/ty3/pr3_props.ma LambdaDelta-1/ty3/pr3.ma
+LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pr1/defs.ma
+LambdaDelta-2/iso/props.ma LambdaDelta-2/iso/props.mma
+LambdaDelta-1/drop/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/lift/defs.ma LambdaDelta-1/r/defs.ma
+LambdaDelta-2/tlist/props.ma LambdaDelta-2/tlist/props.mma
+LambdaDelta-2/subst0/defs.mma LambdaDelta-2/lift/defs.ma
+LambdaDelta-2/clear/props.ma LambdaDelta-2/clear/props.mma
+LambdaDelta-2/subst0/subst0.ma LambdaDelta-2/subst0/subst0.mma
+LambdaDelta-2/s/props.ma LambdaDelta-2/s/props.mma
+LambdaDelta-2/csubst0/defs.ma LambdaDelta-2/csubst0/defs.mma
+LambdaDelta-2/asucc/defs.mma LambdaDelta-2/A/defs.ma LambdaDelta-2/G/defs.ma
+LambdaDelta-2/lift/fwd.mma LambdaDelta-1/lift/fwd.ma LambdaDelta-2/lift/defs.ma
+LambdaDelta-1/ty3/props.ma LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/ty3/fwd.ma
+LambdaDelta-2/r/props.ma LambdaDelta-2/r/props.mma
+LambdaDelta-2/drop1/fwd.mma LambdaDelta-1/drop1/fwd.ma LambdaDelta-2/drop1/defs.ma
+LambdaDelta-2/ty3/pr3_props.mma LambdaDelta-1/ty3/pr3_props.ma LambdaDelta-2/ty3/pr3.ma
+LambdaDelta-2/C/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/sty0/props.mma LambdaDelta-1/sty0/props.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/sty0/defs.ma
+LambdaDelta-2/pc3/wcpr0.ma LambdaDelta-2/pc3/wcpr0.mma
+LambdaDelta-2/arity/props.ma LambdaDelta-2/arity/props.mma
+LambdaDelta-2/csubst0/drop.mma LambdaDelta-1/csubst0/drop.ma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/s/props.ma
+LambdaDelta-1/app/defs.ma LambdaDelta-1/C/defs.ma
+LambdaDelta-2/wcpr0/getl.ma LambdaDelta-2/wcpr0/getl.mma
+LambdaDelta-2/pc1/props.ma LambdaDelta-2/pc1/props.mma
+Base-2/ext/tactics.mma Base-1/ext/tactics.ma Base-2/preamble.ma
+LambdaDelta-2/aplus/props.ma LambdaDelta-2/aplus/props.mma
+LambdaDelta-2/pr2/subst1.mma LambdaDelta-1/pr2/subst1.ma LambdaDelta-2/csubst1/fwd.ma LambdaDelta-2/csubst1/getl.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/pr0/subst1.ma LambdaDelta-2/pr2/defs.ma LambdaDelta-2/subst1/subst1.ma
+LambdaDelta-1/ty3/fsubst0.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/pc3/fsubst0.ma LambdaDelta-1/ty3/props.ma
+LambdaDelta-1/aprem/defs.ma LambdaDelta-1/A/defs.ma
+LambdaDelta-2/tlt/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-1/arity/defs.ma LambdaDelta-1/getl/defs.ma LambdaDelta-1/leq/defs.ma
+LambdaDelta-2/wf3/defs.mma LambdaDelta-2/ty3/defs.ma
+LambdaDelta-2/pr1/pr1.ma LambdaDelta-2/pr1/pr1.mma
+LambdaDelta-2/A/defs.mma LambdaDelta-2/preamble.ma
+LambdaDelta-1/arity/pr3.ma LambdaDelta-1/arity/subst0.ma LambdaDelta-1/csuba/arity.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr3/defs.ma LambdaDelta-1/wcpr0/getl.ma
+LambdaDelta-2/drop1/props.mma LambdaDelta-1/drop1/props.ma LambdaDelta-2/drop/props.ma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/getl/defs.ma
+LambdaDelta-1/wcpr0/fwd.ma LambdaDelta-1/wcpr0/defs.ma
+LambdaDelta-2/getl/drop.mma LambdaDelta-1/getl/drop.ma LambdaDelta-2/clear/drop.ma LambdaDelta-2/getl/props.ma
+LambdaDelta-2/pc3/left.ma LambdaDelta-2/pc3/left.mma
+LambdaDelta-1/ty3/subst1.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/pc3/subst1.ma LambdaDelta-1/ty3/props.ma
+Legacy-1/preamble.ma 
+LambdaDelta-1/pr3/pr3.ma LambdaDelta-1/pr2/pr2.ma LambdaDelta-1/pr3/props.ma
+Base-1/ext/arith.ma Base-1/preamble.ma
+LambdaDelta-1/llt/props.ma LambdaDelta-1/leq/defs.ma LambdaDelta-1/llt/defs.ma
+Base-1/plist/defs.ma Base-1/preamble.ma
+LambdaDelta-2/nf2/iso.ma LambdaDelta-2/nf2/iso.mma
+LambdaDelta-2/iso/fwd.mma LambdaDelta-1/iso/fwd.ma LambdaDelta-2/iso/defs.ma LambdaDelta-2/tlist/defs.ma
+LambdaDelta-1/csubst0/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/subst0/defs.ma
+LambdaDelta-2/csubc/fwd.mma LambdaDelta-1/csubc/fwd.ma LambdaDelta-2/csubc/defs.ma
+LambdaDelta-2/pc3/fwd.mma LambdaDelta-1/pc3/fwd.ma LambdaDelta-2/pc3/props.ma LambdaDelta-2/pr3/fwd.ma
+LambdaDelta-2/fsubst0/defs.ma LambdaDelta-2/fsubst0/defs.mma
+LambdaDelta-1/sty0/fwd.ma LambdaDelta-1/sty0/defs.ma
+LambdaDelta-2/pc1/props.mma LambdaDelta-1/pc1/props.ma LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pr1/pr1.ma
+LambdaDelta-1/csubc/drop1.ma LambdaDelta-1/csubc/drop.ma
+LambdaDelta-2/csuba/fwd.ma LambdaDelta-2/csuba/fwd.mma
+LambdaDelta-2/drop/props.ma LambdaDelta-2/drop/props.mma
+LambdaDelta-2/subst0/tlt.ma LambdaDelta-2/subst0/tlt.mma
+LambdaDelta-1/pr3/subst1.ma LambdaDelta-1/pr2/subst1.ma LambdaDelta-1/pr3/defs.ma
+LambdaDelta-2/csubt/ty3.mma LambdaDelta-1/csubt/ty3.ma LambdaDelta-2/csubt/pc3.ma LambdaDelta-2/csubt/props.ma
+LambdaDelta-2/csubt/csuba.mma LambdaDelta-1/csubt/csuba.ma LambdaDelta-2/ty3/arity.ma
+LambdaDelta-1/clear/defs.ma LambdaDelta-1/C/defs.ma
+LambdaDelta-1/pr3/props.ma LambdaDelta-1/pr1/props.ma LambdaDelta-1/pr2/props.ma LambdaDelta-1/pr3/pr1.ma
+LambdaDelta-2/arity/props.mma LambdaDelta-1/arity/props.ma LambdaDelta-2/arity/fwd.ma
+LambdaDelta-2/sn3/props.ma LambdaDelta-2/sn3/props.mma
+LambdaDelta-1/getl/defs.ma LambdaDelta-1/clear/defs.ma LambdaDelta-1/drop/defs.ma
+LambdaDelta-2/pr3/wcpr0.mma LambdaDelta-1/pr3/wcpr0.ma LambdaDelta-2/pr3/props.ma LambdaDelta-2/wcpr0/getl.ma
+LambdaDelta-1/wf3/clear.ma LambdaDelta-1/wf3/fwd.ma
+LambdaDelta-1/getl/props.ma LambdaDelta-1/clear/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/getl/fwd.ma
+LambdaDelta-1/clear/fwd.ma LambdaDelta-1/clear/defs.ma
+LambdaDelta-2/pc3/props.mma LambdaDelta-1/pc3/props.ma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/pr3/pr3.ma
+LambdaDelta-1/preamble.ma Base-1/theory.ma
+LambdaDelta-2/asucc/defs.ma LambdaDelta-2/asucc/defs.mma
+LambdaDelta-1/pr2/props.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/pr0/props.ma LambdaDelta-1/pr2/defs.ma
+LambdaDelta-1/ex2/defs.ma LambdaDelta-1/C/defs.ma
+LambdaDelta-1/arity/lift1.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/drop1/fwd.ma
+LambdaDelta-1/leq/asucc.ma LambdaDelta-1/leq/props.ma
+LambdaDelta-2/getl/getl.ma LambdaDelta-2/getl/getl.mma
+LambdaDelta-1/next_plus/defs.ma LambdaDelta-1/G/defs.ma
+LambdaDelta-2/cimp/props.ma LambdaDelta-2/cimp/props.mma
+LambdaDelta-2/ex1/props.mma LambdaDelta-1/ex1/props.ma LambdaDelta-2/arity/defs.ma LambdaDelta-2/ex1/defs.ma LambdaDelta-2/leq/props.ma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/nf2/props.ma LambdaDelta-2/pc3/fwd.ma LambdaDelta-2/ty3/fwd.ma
+LambdaDelta-1/subst/defs.ma LambdaDelta-1/lift/defs.ma
+LambdaDelta-2/lift1/props.ma LambdaDelta-2/lift1/props.mma
+LambdaDelta-2/cnt/defs.ma LambdaDelta-2/cnt/defs.mma
+LambdaDelta-2/wcpr0/getl.mma LambdaDelta-1/wcpr0/getl.ma LambdaDelta-2/getl/props.ma LambdaDelta-2/wcpr0/defs.ma
+LambdaDelta-2/subst/props.mma LambdaDelta-1/subst/props.ma LambdaDelta-2/lift/props.ma LambdaDelta-2/subst/fwd.ma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-2/lift/props.mma LambdaDelta-1/lift/props.ma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/s/props.ma
+LambdaDelta-2/csubc/drop.mma LambdaDelta-1/csubc/drop.ma LambdaDelta-2/csubc/fwd.ma LambdaDelta-2/sc3/props.ma
+LambdaDelta-1/pr3/wcpr0.ma LambdaDelta-1/pr3/props.ma LambdaDelta-1/wcpr0/getl.ma
+LambdaDelta-2/subst1/props.ma LambdaDelta-2/subst1/props.mma
+LambdaDelta-2/leq/props.ma LambdaDelta-2/leq/props.mma
+LambdaDelta-2/pr1/defs.ma LambdaDelta-2/pr1/defs.mma
+LambdaDelta-2/csubst1/getl.mma LambdaDelta-1/csubst1/getl.ma LambdaDelta-2/csubst0/getl.ma LambdaDelta-2/csubst1/props.ma LambdaDelta-2/drop/props.ma LambdaDelta-2/subst1/props.ma
+LambdaDelta-2/arity/subst0.ma LambdaDelta-2/arity/subst0.mma
+LambdaDelta-2/getl/props.mma LambdaDelta-1/getl/props.ma LambdaDelta-2/clear/props.ma LambdaDelta-2/drop/props.ma LambdaDelta-2/getl/fwd.ma
+LambdaDelta-2/cnt/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-1/spare.ma LambdaDelta-1/theory.ma
+LambdaDelta-1/pr1/props.ma LambdaDelta-1/T/props.ma LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/subst1/props.ma
+LambdaDelta-2/sty0/defs.ma LambdaDelta-2/sty0/defs.mma
+LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/csubst0/defs.ma
+LambdaDelta-1/flt/props.ma LambdaDelta-1/C/props.ma LambdaDelta-1/flt/defs.ma
+LambdaDelta-1/s/props.ma LambdaDelta-1/s/defs.ma
+LambdaDelta-2/subst0/props.ma LambdaDelta-2/subst0/props.mma
+LambdaDelta-1/flt/defs.ma LambdaDelta-1/C/defs.ma
+LambdaDelta-2/csubst1/fwd.mma LambdaDelta-1/csubst1/fwd.ma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/csubst1/defs.ma LambdaDelta-2/subst1/props.ma
+LambdaDelta-2/csubst0/getl.mma LambdaDelta-1/csubst0/getl.ma LambdaDelta-2/csubst0/clear.ma LambdaDelta-2/csubst0/drop.ma LambdaDelta-2/getl/fwd.ma
+LambdaDelta-1/csubc/clear.ma LambdaDelta-1/csubc/fwd.ma
+LambdaDelta-2/G/defs.ma LambdaDelta-2/G/defs.mma
+LambdaDelta-1/subst0/defs.ma LambdaDelta-1/lift/defs.ma
+LambdaDelta-2/cimp/defs.ma LambdaDelta-2/cimp/defs.mma
+LambdaDelta-2/theory.ma LambdaDelta-2/csubt/csuba.ma LambdaDelta-2/ex0/props.ma LambdaDelta-2/ex1/props.ma LambdaDelta-2/ex2/props.ma LambdaDelta-2/pr3/wcpr0.ma LambdaDelta-2/sty1/cnt.ma LambdaDelta-2/subst/props.ma LambdaDelta-2/subst0/tlt.ma LambdaDelta-2/ty3/fwd_nf2.ma LambdaDelta-2/ty3/nf2.ma LambdaDelta-2/ty3/sty0.ma LambdaDelta-2/wcpr0/fwd.ma LambdaDelta-2/wf3/props.ma
+LambdaDelta-1/pr0/props.ma LambdaDelta-1/pr0/defs.ma LambdaDelta-1/subst0/subst0.ma
+LambdaDelta-1/C/defs.ma LambdaDelta-1/T/defs.ma
+LambdaDelta-1/r/props.ma LambdaDelta-1/r/defs.ma LambdaDelta-1/s/defs.ma
+LambdaDelta-2/lift/defs.ma LambdaDelta-2/lift/defs.mma
+LambdaDelta-2/drop1/defs.ma LambdaDelta-2/drop1/defs.mma
+LambdaDelta-2/subst0/fwd.mma LambdaDelta-1/subst0/fwd.ma LambdaDelta-2/lift/props.ma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-1/sty1/props.ma LambdaDelta-1/sty0/props.ma LambdaDelta-1/sty1/defs.ma
+LambdaDelta-2/getl/flt.mma LambdaDelta-1/getl/flt.ma LambdaDelta-2/clear/props.ma LambdaDelta-2/flt/props.ma LambdaDelta-2/getl/fwd.ma
+LambdaDelta-2/C/props.ma LambdaDelta-2/C/props.mma
+LambdaDelta-2/csuba/drop.mma LambdaDelta-1/csuba/drop.ma LambdaDelta-2/csuba/fwd.ma LambdaDelta-2/drop/fwd.ma
+LambdaDelta-2/clen/defs.ma LambdaDelta-2/clen/defs.mma
+LambdaDelta-1/csubc/csuba.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/props.ma
+LambdaDelta-2/sn3/nf2.mma LambdaDelta-1/sn3/nf2.ma LambdaDelta-2/nf2/dec.ma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/sn3/defs.ma
+LambdaDelta-2/sty1/cnt.ma LambdaDelta-2/sty1/cnt.mma
+LambdaDelta-2/pr3/pr1.ma LambdaDelta-2/pr3/pr1.mma
+LambdaDelta-2/getl/dec.mma LambdaDelta-1/getl/dec.ma LambdaDelta-2/getl/props.ma
+LambdaDelta-2/fsubst0/defs.mma LambdaDelta-2/csubst0/defs.ma
+LambdaDelta-2/wf3/getl.ma LambdaDelta-2/wf3/getl.mma
+LambdaDelta-2/wf3/fwd.ma LambdaDelta-2/wf3/fwd.mma
+LambdaDelta-1/csubt/getl.ma LambdaDelta-1/csubt/clear.ma LambdaDelta-1/csubt/drop.ma LambdaDelta-1/getl/clear.ma
+LambdaDelta-1/csubv/props.ma LambdaDelta-1/T/props.ma LambdaDelta-1/csubv/defs.ma
+LambdaDelta-1/lift1/fwd.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/lift1/defs.ma
+LambdaDelta-1/sty0/props.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/sty0/defs.ma
+LambdaDelta-2/tlist/props.mma LambdaDelta-1/tlist/props.ma LambdaDelta-2/tlist/defs.ma
+LambdaDelta-2/csubv/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/csubt/drop.ma LambdaDelta-2/csubt/drop.mma
+LambdaDelta-1/ty3/defs.ma LambdaDelta-1/G/defs.ma LambdaDelta-1/pc3/defs.ma
+LambdaDelta-2/getl/getl.mma LambdaDelta-1/getl/getl.ma LambdaDelta-2/getl/clear.ma LambdaDelta-2/getl/drop.ma
+LambdaDelta-2/ty3/subst1.mma LambdaDelta-1/ty3/subst1.ma LambdaDelta-2/getl/getl.ma LambdaDelta-2/pc3/subst1.ma LambdaDelta-2/ty3/props.ma
+LambdaDelta-2/nf2/lift1.ma LambdaDelta-2/nf2/lift1.mma
+LambdaDelta-1/ex2/props.ma LambdaDelta-1/arity/fwd.ma LambdaDelta-1/ex2/defs.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/fwd.ma
+LambdaDelta-2/ty3/fsubst0.mma LambdaDelta-1/ty3/fsubst0.ma LambdaDelta-2/getl/getl.ma LambdaDelta-2/pc3/fsubst0.ma LambdaDelta-2/ty3/props.ma
+LambdaDelta-2/subst0/subst0.mma LambdaDelta-1/subst0/subst0.ma LambdaDelta-2/subst0/props.ma
+LambdaDelta-1/csuba/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csuba/defs.ma
+LambdaDelta-1/subst1/props.ma LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst1/defs.ma
+LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/drop1/fwd.mma
+LambdaDelta-2/csubc/fwd.ma LambdaDelta-2/csubc/fwd.mma
+LambdaDelta-1/pr0/defs.ma LambdaDelta-1/subst0/defs.ma
+LambdaDelta-2/sc3/defs.mma LambdaDelta-2/arity/defs.ma LambdaDelta-2/drop1/defs.ma LambdaDelta-2/sn3/defs.ma
+LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/defs.ma
+LambdaDelta-1/csuba/getl.ma LambdaDelta-1/csuba/clear.ma LambdaDelta-1/csuba/drop.ma LambdaDelta-1/getl/clear.ma
+LambdaDelta-2/lift/fwd.ma LambdaDelta-2/lift/fwd.mma
+LambdaDelta-2/clear/drop.mma LambdaDelta-1/clear/drop.ma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/drop/fwd.ma
+LambdaDelta-2/csubv/defs.ma LambdaDelta-2/csubv/defs.mma
+LambdaDelta-2/csuba/drop.ma LambdaDelta-2/csuba/drop.mma
+LambdaDelta-1/pr1/pr1.ma LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/pr1/props.ma
+LambdaDelta-1/nf2/arity.ma LambdaDelta-1/arity/subst0.ma LambdaDelta-1/nf2/fwd.ma
+LambdaDelta-2/T/props.mma LambdaDelta-1/T/props.ma LambdaDelta-2/T/defs.ma
+Legacy-1/coq/props.ma Legacy-1/coq/defs.ma
+LambdaDelta-2/ty3/fsubst0.ma LambdaDelta-2/ty3/fsubst0.mma
+LambdaDelta-2/sn3/fwd.ma LambdaDelta-2/sn3/fwd.mma
+LambdaDelta-1/pr2/clen.ma LambdaDelta-1/clen/getl.ma LambdaDelta-1/pr2/props.ma
+LambdaDelta-2/ty3/dec.mma LambdaDelta-1/ty3/dec.ma LambdaDelta-2/getl/dec.ma LambdaDelta-2/getl/flt.ma LambdaDelta-2/pc3/dec.ma
+LambdaDelta-2/tlt/props.ma LambdaDelta-2/tlt/props.mma
+LambdaDelta-2/next_plus/props.mma LambdaDelta-1/next_plus/props.ma LambdaDelta-2/next_plus/defs.ma
+LambdaDelta-1/arity/subst0.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/fsubst0/fwd.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/subst0/dec.ma LambdaDelta-1/subst0/fwd.ma
+LambdaDelta-2/pr0/subst1.ma LambdaDelta-2/pr0/subst1.mma
+LambdaDelta-2/lift/defs.mma LambdaDelta-2/s/defs.ma LambdaDelta-2/tlist/defs.ma
+LambdaDelta-1/wf3/defs.ma LambdaDelta-1/ty3/defs.ma
+LambdaDelta-1/ex1/props.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/ex1/defs.ma LambdaDelta-1/leq/props.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/nf2/props.ma LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/ty3/fwd.ma
+LambdaDelta-1/csubt/ty3.ma LambdaDelta-1/csubt/pc3.ma LambdaDelta-1/csubt/props.ma
+Legacy-1/spare.ma Legacy-1/theory.ma
+LambdaDelta-2/wf3/props.ma LambdaDelta-2/wf3/props.mma
+LambdaDelta-2/pr0/dec.mma LambdaDelta-1/pr0/dec.ma LambdaDelta-2/T/dec.ma LambdaDelta-2/T/props.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/subst0/dec.ma
+LambdaDelta-2/csubst0/clear.ma LambdaDelta-2/csubst0/clear.mma
+LambdaDelta-1/sc3/defs.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/sn3/defs.ma
+LambdaDelta-2/nf2/dec.mma LambdaDelta-1/nf2/dec.ma LambdaDelta-2/C/props.ma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr0/dec.ma LambdaDelta-2/pr2/clen.ma LambdaDelta-2/pr2/fwd.ma
+LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst0/fwd.ma
+LambdaDelta-1/getl/flt.ma LambdaDelta-1/clear/props.ma LambdaDelta-1/flt/props.ma LambdaDelta-1/getl/fwd.ma
+Base-2/types/defs.ma Base-2/types/defs.mma
+LambdaDelta-1/csubv/drop.ma LambdaDelta-1/csubv/props.ma LambdaDelta-1/drop/fwd.ma
+LambdaDelta-2/ty3/fwd.ma LambdaDelta-2/ty3/fwd.mma
+LambdaDelta-2/s/props.mma LambdaDelta-1/s/props.ma LambdaDelta-2/s/defs.ma
+LambdaDelta-1/csubt/props.ma LambdaDelta-1/csubt/defs.ma
+LambdaDelta-1/nf2/iso.ma LambdaDelta-1/iso/props.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/pr3/fwd.ma
+LambdaDelta-2/arity/aprem.mma LambdaDelta-1/arity/aprem.ma LambdaDelta-2/aprem/props.ma LambdaDelta-2/arity/cimp.ma LambdaDelta-2/arity/props.ma
+LambdaDelta-1/arity/cimp.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/cimp/props.ma
+LambdaDelta-2/csubc/defs.ma LambdaDelta-2/csubc/defs.mma
+LambdaDelta-2/csubt/defs.mma LambdaDelta-2/ty3/defs.ma
+LambdaDelta-2/iso/defs.ma LambdaDelta-2/iso/defs.mma
+LambdaDelta-2/ty3/fwd_nf2.mma LambdaDelta-1/ty3/fwd_nf2.ma LambdaDelta-2/nf2/fwd.ma LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/ty3/arity_props.ma
+LambdaDelta-1/llt/defs.ma LambdaDelta-1/A/defs.ma
+LambdaDelta-2/pc3/defs.ma LambdaDelta-2/pc3/defs.mma
+LambdaDelta-2/cimp/props.mma LambdaDelta-1/cimp/props.ma LambdaDelta-2/cimp/defs.ma LambdaDelta-2/getl/getl.ma
+LambdaDelta-2/aplus/props.mma LambdaDelta-1/aplus/props.ma LambdaDelta-2/aplus/defs.ma LambdaDelta-2/next_plus/props.ma
+LambdaDelta-2/getl/clear.mma LambdaDelta-1/getl/clear.ma LambdaDelta-2/clear/drop.ma LambdaDelta-2/getl/props.ma
+LambdaDelta-1/ex0/props.ma LambdaDelta-1/aplus/props.ma LambdaDelta-1/ex0/defs.ma LambdaDelta-1/leq/defs.ma
+LambdaDelta-2/csubc/drop1.mma LambdaDelta-1/csubc/drop1.ma LambdaDelta-2/csubc/drop.ma
+LambdaDelta-1/pc3/fsubst0.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/pc3/left.ma
+LambdaDelta-1/csubc/drop.ma LambdaDelta-1/csubc/fwd.ma LambdaDelta-1/sc3/props.ma
+LambdaDelta-2/pr2/subst1.ma LambdaDelta-2/pr2/subst1.mma
+LambdaDelta-2/ty3/arity.mma LambdaDelta-1/ty3/arity.ma LambdaDelta-2/arity/pr3.ma LambdaDelta-2/asucc/fwd.ma LambdaDelta-2/ty3/pr3_props.ma
+LambdaDelta-2/pc3/fwd.ma LambdaDelta-2/pc3/fwd.mma
+LambdaDelta-1/nf2/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/fwd.ma
+Base-1/blt/defs.ma Base-1/preamble.ma
+LambdaDelta-2/nf2/iso.mma LambdaDelta-1/nf2/iso.ma LambdaDelta-2/iso/props.ma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/pr3/fwd.ma
+LambdaDelta-2/csubc/drop1.ma LambdaDelta-2/csubc/drop1.mma
+LambdaDelta-2/csubc/getl.mma LambdaDelta-1/csubc/getl.ma LambdaDelta-2/csubc/clear.ma LambdaDelta-2/csubc/drop.ma
+LambdaDelta-2/getl/clear.ma LambdaDelta-2/getl/clear.mma
+LambdaDelta-1/ty3/fwd_nf2.ma LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/ty3/arity_props.ma
+LambdaDelta-2/getl/fwd.ma LambdaDelta-2/getl/fwd.mma
+LambdaDelta-2/tlt/props.mma LambdaDelta-1/tlt/props.ma LambdaDelta-2/tlt/defs.ma
+Base-1/preamble.ma Legacy-1/theory.ma
+LambdaDelta-2/ex1/defs.ma LambdaDelta-2/ex1/defs.mma
+LambdaDelta-2/csubc/csuba.mma LambdaDelta-1/csubc/csuba.ma LambdaDelta-2/csubc/defs.ma LambdaDelta-2/sc3/props.ma
+LambdaDelta-2/subst/fwd.ma LambdaDelta-2/subst/fwd.mma
+LambdaDelta-2/clen/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/s/defs.ma
+LambdaDelta-2/iso/props.mma LambdaDelta-1/iso/props.ma LambdaDelta-2/iso/fwd.ma
+LambdaDelta-1/drop/fwd.ma LambdaDelta-1/drop/defs.ma
+LambdaDelta-2/csubt/fwd.mma LambdaDelta-1/csubt/fwd.ma LambdaDelta-2/csubt/defs.ma
+Base-1/blt/props.ma Base-1/blt/defs.ma
+LambdaDelta-1/pr3/defs.ma LambdaDelta-1/pr2/defs.ma
+LambdaDelta-2/s/defs.ma LambdaDelta-2/s/defs.mma
+LambdaDelta-2/lift1/props.mma LambdaDelta-1/lift1/props.ma LambdaDelta-2/drop1/defs.ma LambdaDelta-2/lift/props.ma
+LambdaDelta-1/aprem/fwd.ma LambdaDelta-1/aprem/defs.ma
+LambdaDelta-2/ty3/arity_props.ma LambdaDelta-2/ty3/arity_props.mma
+Base-1/plist/props.ma Base-1/plist/defs.ma
+LambdaDelta-2/arity/lift1.ma LambdaDelta-2/arity/lift1.mma
+LambdaDelta-1/wcpr0/getl.ma LambdaDelta-1/getl/props.ma LambdaDelta-1/wcpr0/defs.ma
+LambdaDelta-2/pr2/fwd.mma LambdaDelta-1/pr2/fwd.ma LambdaDelta-2/getl/clear.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/pr2/defs.ma
+Base-1/ext/tactics.ma Base-1/preamble.ma
+LambdaDelta-1/drop1/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/getl/defs.ma
diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index d8d498a32..129f2dabd 100644
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -166,68 +166,14 @@ let usage () =
   try Hashtbl.find usages usage_key with Not_found -> default_usage
 ;;
 
-let dump f =
-   let module G = GrafiteAst in
-   let module L = LexiconAst in
-   let module H = HExtlib in
-   Helm_registry.set_bool "matita.moo" false;
-   let floc = H.dummy_floc in
-   let nl_ast = G.Comment (floc, G.Note (floc, "")) in
-   let och = open_out f in
-   let atexit () = close_out och in
-   let out_comment och s =
-      let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in 
-      Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
-   in
-   let out_line_comment och s =
-      let l = 70 - String.length s in
-      let s = Printf.sprintf " %s %s" s (String.make l '*') in
-      out_comment och s
-   in
-   let out_preamble och (path, lines) =
-      let ich = open_in path in
-      let rec print i =
-         if i > 0 then 
-            let s = input_line ich in
-            begin Printf.fprintf och "%s\n" s; print (pred i) end
-      in 
-      print lines;
-      out_line_comment och "This file was automatically generated: do not edit"
-   in
-   let pp_ast_statement st =
-     GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
-       ~map_unicode_to_tex:(Helm_registry.get_bool
-         "matita.paste_unicode_as_tex")
-       ~lazy_term_pp:CicNotationPp.pp_term 
-       ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
-   in
-   let nl () =  output_string och (pp_ast_statement nl_ast) in
-   let rt_base_dir = Filename.dirname Sys.argv.(0) in
-   let path = Filename.concat rt_base_dir "matita.ma.templ" in
-   let lines = 14 in
-   out_preamble och (path, lines);
-   let grafite_parser_cb fname = 
-      let ast = G.Executable 
-        (floc, G.Command (floc, G.Include (floc, fname))) in
-      output_string och (pp_ast_statement ast); nl (); nl ()
-   in
-   let matita_engine_cb = function
-      | G.Executable (_, G.Macro (_, G.Inline _)) 
-      | G.Executable (_, G.Command (_, G.Include _)) -> ()
-      | ast                                          ->
-         output_string och (pp_ast_statement ast); nl (); nl ()
-   in
-   let matitac_lib_cb = output_string och in
-   GrafiteParser.set_callback grafite_parser_cb;
-   MatitaEngine.set_callback matita_engine_cb;
-   MatitacLib.set_callback matitac_lib_cb;
-   at_exit atexit
-;;
-
 let extra_cmdline_specs = ref []
 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
 
 let parse_cmdline init_status =
+  let dump fname = 
+     let atexit = MatitacLib.dump fname in
+     at_exit atexit
+  in
   if not (already_configured [CmdLine] init_status) then begin
     wants [Registry] init_status;
     let includes = ref [] in
diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 7790f7568..b33590a0a 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -34,6 +34,7 @@ exception AttemptToInsertAnAlias of LexiconEngine.status
 let out = ref ignore 
 let set_callback f = out := f
 
+
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
 let pp_ast_statement grafite_status stm =
@@ -55,6 +56,67 @@ let clean_exit baseuri rc =
   LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc
 ;;
 
+let dump f =
+   let module G = GrafiteAst in
+   let module L = LexiconAst in
+   let module H = HExtlib in
+   Helm_registry.set_bool "matita.moo" false;
+   let floc = H.dummy_floc in
+   let nl_ast = G.Comment (floc, G.Note (floc, "")) in
+   let och = open_out f in
+   let out_comment och s =
+      let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in 
+      Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
+   in
+   let out_line_comment och s =
+      let l = 70 - String.length s in
+      let s = Printf.sprintf " %s %s" s (String.make l '*') in
+      out_comment och s
+   in
+   let out_preamble och (path, lines) =
+      let ich = open_in path in
+      let rec print i =
+         if i > 0 then 
+            let s = input_line ich in
+            begin Printf.fprintf och "%s\n" s; print (pred i) end
+      in 
+      print lines;
+      out_line_comment och "This file was automatically generated: do not edit"
+   in
+   let pp_ast_statement st =
+     GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+       ~map_unicode_to_tex:(Helm_registry.get_bool
+         "matita.paste_unicode_as_tex")
+       ~lazy_term_pp:CicNotationPp.pp_term 
+       ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
+   in
+   let nl () =  output_string och (pp_ast_statement nl_ast) in
+   let rt_base_dir = Filename.dirname Sys.argv.(0) in
+   let path = Filename.concat rt_base_dir "matita.ma.templ" in
+   let lines = 14 in
+   out_preamble och (path, lines);
+   let grafite_parser_cb fname = 
+      let ast = G.Executable 
+        (floc, G.Command (floc, G.Include (floc, fname))) in
+      output_string och (pp_ast_statement ast); nl (); nl ()
+   in
+   let matita_engine_cb = function
+      | G.Executable (_, G.Macro (_, G.Inline _)) 
+      | G.Executable (_, G.Command (_, G.Include _)) -> ()
+      | ast                                          ->
+         output_string och (pp_ast_statement ast); nl (); nl ()
+   in
+   let matitac_lib_cb = output_string och in
+   GrafiteParser.set_callback grafite_parser_cb;
+   MatitaEngine.set_callback matita_engine_cb;
+   set_callback matitac_lib_cb;
+   fun x ->
+      close_out och;
+      GrafiteParser.set_callback ignore;
+      MatitaEngine.set_callback ignore;
+      set_callback ignore; x
+;;
+
 let get_macro_context = function
    | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
    | Some status                ->
@@ -286,8 +348,14 @@ module F =
         let root,baseuri,_,_ =
           Librarian.baseuri_of_script ~include_paths mafile 
         in
-        Some root, LibraryMisc.obj_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:true 
+	let obj =
+	   if Filename.check_suffix mafile ".mma" then 
+	      Filename.chop_suffix mafile ".mma" ^ ".ma"
+	   else
+	      LibraryMisc.obj_file_of_baseuri 
+                 ~must_exist:false ~baseuri ~writable:true
+	in
+        Some root, obj 
       with Librarian.NoRootFor x -> None, ""
 
     let mtime_of_source_object s =
@@ -298,9 +366,16 @@ module F =
       try Some (Unix.stat s).Unix.st_mtime
       with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
 
-    let build = compile;;
+    let build options fname =
+       if Filename.check_suffix fname ".mma" then 
+          let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
+	  let atexit = dump generated in
+	  let res = compile options fname in
+	  atexit res
+       else
+          compile options fname
 
-    let load_deps_file = Librarian.load_deps_file;;
+    let load_deps_file = Librarian.load_deps_file
 
   end 
 
diff --git a/helm/software/matita/matitacLib.mli b/helm/software/matita/matitacLib.mli
index 03ea56beb..034aaedaf 100644
--- a/helm/software/matita/matitacLib.mli
+++ b/helm/software/matita/matitacLib.mli
@@ -23,8 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
-(* this callback is called on the expansion of every inline macro *)
-val set_callback: (string -> unit) -> unit 
+(* ma from mma generation: ma file -> atexit function *)
+val dump: string -> 'a -> 'a
 
 module Make : sig
         val make: string -> string list -> bool
diff --git a/helm/software/matita/matitadep.ml b/helm/software/matita/matitadep.ml
index d50707f29..c0d784637 100644
--- a/helm/software/matita/matitadep.ml
+++ b/helm/software/matita/matitadep.ml
@@ -59,14 +59,19 @@ let main () =
   let set_dot_file () = dot_file := dot_name^".dot" in
   let set_excluded_file name = excluded_files := name :: !excluded_files in 
   (* helpers *)
-  let baseuri_of_script s = 
+  let rec baseuri_of_script s = 
      try Hashtbl.find baseuri_of s 
      with Not_found -> 
-       let _,b,_,_ = 
+       let _,b,_,_ =  
          Librarian.baseuri_of_script ~include_paths:!include_paths s 
        in
        Hashtbl.add baseuri_of s b; 
        Hashtbl.add baseuri_of_inv b s; 
+       let _ =
+          if Filename.check_suffix s ".mma" then
+	     let generated = Filename.chop_suffix s ".mma" ^ ".ma" in
+	     ignore (baseuri_of_script generated)
+       in
        b
   in
   let script_of_baseuri ma b =
@@ -95,8 +100,11 @@ let main () =
   MatitaInit.initialize_environment ();
   if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
   let cmdline_args = HR.get_list HR.string "matita.args" in
+  let test x =
+     Filename.check_suffix x ".ma" || Filename.check_suffix x ".mma"
+  in
   let files = fun () -> match cmdline_args with
-     | [] -> HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "."
+     | [] -> HExtlib.find ~test "."
      | _  -> cmdline_args
   in
   let args = 
@@ -129,10 +137,19 @@ let main () =
 (*  let _ = print_times "prima di iter1" in *)
   List.iter (fun ma_file -> ignore (baseuri_of_script ma_file)) ma_files;
 (*  let _ = print_times "in mezzo alle due iter" in *)
+  let map s _ l = s :: l in
+  let ma_files = Hashtbl.fold map baseuri_of [] in
   List.iter
    (fun ma_file -> 
+      let _ = if Filename.check_suffix ma_file ".mma" then
+         let generated = Filename.chop_suffix ma_file ".mma" ^ ".ma" in
+         Hashtbl.add include_deps generated ma_file;
+      in
       let ma_baseuri = baseuri_of_script ma_file in
-      let dependencies = DependenciesParser.deps_of_file ma_file in
+      let dependencies = 
+         try DependenciesParser.deps_of_file ma_file
+	 with Sys_error _ -> []
+      in
       List.iter 
        (function
          | DependenciesParser.UriDep uri -> 
@@ -145,7 +162,8 @@ let main () =
                   match script_of_baseuri ma_file u with
                   | Some d -> Hashtbl.add include_deps ma_file d
                   | None -> ())                
-         | DependenciesParser.IncludeDep path -> 
+         | DependenciesParser.InlineDep path
+	 | DependenciesParser.IncludeDep path -> 
                 ignore (baseuri_of_script path);
                 Hashtbl.add include_deps ma_file path)
        dependencies)
diff --git a/helm/software/matita/tests/fguidi.ma b/helm/software/matita/tests/fguidi.ma
index 966ff7cc2..c0aa6b284 100644
--- a/helm/software/matita/tests/fguidi.ma
+++ b/helm/software/matita/tests/fguidi.ma
@@ -15,33 +15,8 @@
 include "logic/connectives.ma".
 include "nat/nat.ma".
 
-definition is_S: nat \to Prop \def
-   \lambda n. match n with 
-      [ O     \Rightarrow False
-      | (S n) \Rightarrow True
-      ].
-
-definition pred: nat \to nat \def
-   \lambda n. match n with
-      [ O     \Rightarrow O
-      | (S n) \Rightarrow n
-      ]. 
-
-theorem eq_gen_S_O: \forall x. (S x = O) \to \forall P:Prop. P.
-intros. apply False_ind. cut (is_S O). elim Hcut. rewrite < H. apply I.
-qed.
-
-theorem eq_gen_S_O_cc: (\forall P:Prop. P) \to \forall x. (S x = O).
-intros. apply H.
-qed.
-
-theorem eq_gen_S_S: \forall m,n. (S m) = (S n) \to m = n. 
-intros. cut ((pred (S m)) = (pred (S n))). 
-assumption. elim H. autobatch.
-qed.
-
-theorem eq_gen_S_S_cc: \forall m,n. m = n \to (S m) = (S n).
-intros. elim H. autobatch.
+theorem eq_S_S: \forall m,n. m = n \to (S m) = (S n).
+intros; destruct; autobatch.
 qed.
 
 inductive le: nat \to nat \to Prop \def
@@ -49,55 +24,57 @@ inductive le: nat \to nat \to Prop \def
    | le_succ: \forall m, n. (le m n) \to (le (S m) (S n)).
 
 theorem le_refl: \forall x. (le x x).
-intros. elim x; autobatch.
+intros; elim x; clear x; autobatch.
 qed.
 
-theorem le_gen_x_O_aux: \forall x, y. (le x y) \to (y =O) \to 
-                        (x = O).
-intros 3. elim H. autobatch. apply eq_gen_S_O. exact n1. autobatch.
+theorem le_gen_x_O_aux: \forall x, y. (le x y) \to (y =O) \to (x = O).
+intros 3; elim H; clear H x y;
+[ autobatch
+| destruct
+]
 qed.
 
 theorem le_gen_x_O: \forall x. (le x O) \to (x = O).
-intros. apply le_gen_x_O_aux. exact O. autobatch. autobatch.
+intros; lapply linear le_gen_x_O_aux to H;
+[ destruct; autobatch
+| autobatch
+].
 qed.
 
-theorem le_gen_x_O_cc: \forall x. (x = O) \to (le x O).
-intros. elim H. autobatch.
+theorem le_x_O: \forall x. (x = O) \to (le x O).
+intros; destruct; autobatch.
 qed.
 
 theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to 
                         (\exists n. x = (S n) \land (le m n)).
-intros 4. elim H; clear H x y.
-apply eq_gen_S_O. exact m. elim H1. autobatch.
-clear H2. cut (n = m).
-elim Hcut. apply ex_intro. exact n1. split; autobatch.
-apply eq_gen_S_S. autobatch.
+intros 4; elim H; clear H x y;
+[ destruct
+| destruct; autobatch
+].
 qed.
 
 theorem le_gen_S_x: \forall m,x. (le (S m) x) \to 
                     (\exists n. x = (S n) \land (le m n)).
-intros. apply le_gen_S_x_aux. exact (S m). autobatch. autobatch.
+intros; lapply le_gen_S_x_aux to H; autobatch.
 qed.
 
-theorem le_gen_S_x_cc: \forall m,x. (\exists n. x = (S n) \land (le m n)) \to
-                       (le (S m) x).
-intros. elim H. elim H1. cut ((S a) = x). elim Hcut. autobatch.
-elim H2. autobatch.
+theorem le_S_x: \forall m,x. (\exists n. x = (S n) \land (le m n)) \to
+                (le (S m) x).
+intros; decompose; destruct; autobatch.
 qed.
 
 theorem le_gen_S_S: \forall m,n. (le (S m) (S n)) \to (le m n).
 intros.
-lapply le_gen_S_x to H as H0. elim H0. elim H1. 
-lapply eq_gen_S_S to H2 as H4. rewrite > H4. assumption.
+lapply linear le_gen_S_x to H as H0; decompose; destruct; autobatch.
 qed.
 
-theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)).
-intros. autobatch.
+theorem le_S_S: \forall m,n. (le m n) \to (le (S m) (S n)).
+intros; autobatch.
 qed.
 
-(*
 theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
-intros 1. elim x; clear H. clear x. 
-autobatch.
-fwd H1 [H]. decompose.
-*)
+intros 3. elim H; clear H x y;
+[ autobatch
+| lapply linear le_gen_S_x to H3; decompose; destruct; autobatch.
+].
+qed.