Procedural: bug fix in comment generation

applyTransformation: now mma compilation fails on procedural generation errors
matitacLib: when the mma fails the generated ma is removed

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 1660df50dd9401d80c445f92388d1271d566c1aa..380e52efec280ca40f308a92b5e0bcafd00c2998 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -92,7 +92,7 @@ let push st = {st with case = 1 :: st.case}
 
 let inc st =
    {st with case = match st.case with 
-      | []       -> assert false
+      | []       -> []
       | hd :: tl -> succ hd :: tl
    }
 

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 2a4624c217b7531ae14bd7b42fcdd8c3a106c9cd..0982757b02d8b38ba933636c85e5a144cb442c32 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -220,8 +220,13 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
           (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
       with
          | e -> 
-            Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
-            (UriManager.string_of_uri uri) (print_exc e)
+            let msg = 
+              Printf.sprintf 
+                 "ERRORE IN STAMPA DI %s\nEXCEPTION: %s" 
+                  (UriManager.string_of_uri uri) (print_exc e)
+           in
+           Printf.eprintf "%s\n" msg;
+           GrafiteTypes.command_error msg
    in
    String.concat "" (List.map map sorted_uris)
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/depends b/helm/software/matita/contribs/LAMBDA-TYPES/depends
index cda04b7150f8648078a9403f67478fb89dfc4b95..a8193b34e1de0a55101973d10180fde4e288af51 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/depends
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/depends
@@ -1,7 +1,7 @@
 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
+LambdaDelta-2/ty3/dec.ma LambdaDelta-2/ty3/dec.mma LambdaDelta-2/getl/dec.ma LambdaDelta-2/getl/flt.ma LambdaDelta-2/pc3/dec.ma
 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
@@ -10,37 +10,37 @@ LambdaDelta-2/sn3/fwd.mma LambdaDelta-1/sn3/fwd.ma LambdaDelta-2/pr3/props.ma La
 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-2/cnt/props.ma LambdaDelta-2/cnt/props.mma LambdaDelta-2/cnt/defs.ma LambdaDelta-2/lift/fwd.ma
+LambdaDelta-2/nf2/fwd.ma LambdaDelta-2/nf2/fwd.mma LambdaDelta-2/T/props.ma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/clen.ma LambdaDelta-2/subst0/dec.ma
+LambdaDelta-2/csubst1/defs.ma LambdaDelta-2/csubst1/defs.mma LambdaDelta-2/csubst0/defs.ma
+LambdaDelta-2/ty3/pr3.ma LambdaDelta-2/ty3/pr3.mma 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-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/sc3/arity.ma LambdaDelta-2/sc3/arity.mma LambdaDelta-2/csubc/arity.ma LambdaDelta-2/csubc/drop1.ma LambdaDelta-2/csubc/getl.ma LambdaDelta-2/csubc/props.ma
 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-2/pc3/dec.ma LambdaDelta-2/pc3/dec.mma LambdaDelta-2/nf2/fwd.ma LambdaDelta-2/ty3/arity_props.ma
 LambdaDelta-1/next_plus/props.ma LambdaDelta-1/next_plus/defs.ma
-LambdaDelta-2/csubt/pc3.ma LambdaDelta-2/csubt/pc3.mma
+LambdaDelta-2/csubt/pc3.ma LambdaDelta-2/csubt/pc3.mma LambdaDelta-2/csubt/getl.ma LambdaDelta-2/pc3/left.ma
 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-2/csubc/clear.ma LambdaDelta-2/csubc/clear.mma LambdaDelta-2/csubc/fwd.ma
+LambdaDelta-2/subst0/defs.ma LambdaDelta-2/subst0/defs.mma LambdaDelta-2/lift/defs.ma
 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-2/ty3/pr3_props.ma LambdaDelta-2/ty3/pr3_props.mma LambdaDelta-2/ty3/pr3.ma
 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/subst0/fwd.ma LambdaDelta-2/subst0/fwd.mma LambdaDelta-2/lift/props.ma LambdaDelta-2/subst0/defs.ma
 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/getl/dec.ma LambdaDelta-2/getl/dec.mma LambdaDelta-2/getl/props.ma
 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/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/csubc/csuba.ma LambdaDelta-2/csubc/csuba.mma LambdaDelta-2/csubc/defs.ma LambdaDelta-2/sc3/props.ma
 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
@@ -50,93 +50,93 @@ 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/csubv/props.ma LambdaDelta-2/csubv/props.mma LambdaDelta-2/T/props.ma LambdaDelta-2/csubv/defs.ma
 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-2/sn3/lift1.ma LambdaDelta-2/sn3/lift1.mma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/lift1/fwd.ma LambdaDelta-2/sn3/props.ma
 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-2/aplus/defs.ma LambdaDelta-2/aplus/defs.mma LambdaDelta-2/asucc/defs.ma
+LambdaDelta-2/sc3/props.ma LambdaDelta-2/sc3/props.mma 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/csuba/clear.ma LambdaDelta-2/csuba/clear.mma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/csuba/defs.ma
 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/getl/drop.ma LambdaDelta-2/getl/drop.mma LambdaDelta-2/clear/drop.ma LambdaDelta-2/getl/props.ma
 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-2/nf2/dec.ma LambdaDelta-2/nf2/dec.mma 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-2/lift/props.ma LambdaDelta-2/lift/props.mma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/s/props.ma
 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/csubt/fwd.ma LambdaDelta-2/csubt/fwd.mma LambdaDelta-2/csubt/defs.ma
+LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/nf2/pr3.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr3/pr3.ma
+LambdaDelta-2/subst1/fwd.ma LambdaDelta-2/subst1/fwd.mma LambdaDelta-2/subst0/props.ma LambdaDelta-2/subst1/defs.ma
 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/csubt/props.ma LambdaDelta-2/csubt/props.mma LambdaDelta-2/csubt/defs.ma
+LambdaDelta-2/pr2/pr2.ma LambdaDelta-2/pr2/pr2.mma LambdaDelta-2/getl/props.ma LambdaDelta-2/pr0/pr0.ma LambdaDelta-2/pr2/defs.ma
 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-2/subst0/dec.ma LambdaDelta-2/subst0/dec.mma LambdaDelta-2/lift/props.ma LambdaDelta-2/subst0/defs.ma
 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/ty3/sty0.ma LambdaDelta-2/ty3/sty0.mma LambdaDelta-2/sty0/fwd.ma LambdaDelta-2/ty3/pr3_props.ma
+LambdaDelta-2/pc3/fsubst0.ma LambdaDelta-2/pc3/fsubst0.mma LambdaDelta-2/csubst0/getl.ma LambdaDelta-2/fsubst0/defs.ma LambdaDelta-2/pc3/left.ma
 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-2/clear/drop.ma LambdaDelta-2/clear/drop.mma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/drop/fwd.ma
 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-2/ty3/fwd_nf2.ma LambdaDelta-2/ty3/fwd_nf2.mma LambdaDelta-2/nf2/fwd.ma LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/ty3/arity_props.ma
 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-2/pr3/iso.ma LambdaDelta-2/pr3/iso.mma LambdaDelta-2/iso/props.ma LambdaDelta-2/pr3/fwd.ma LambdaDelta-2/tlist/props.ma
+LambdaDelta-2/csubt/defs.ma LambdaDelta-2/csubt/defs.mma LambdaDelta-2/ty3/defs.ma
+LambdaDelta-2/pc3/pc1.ma LambdaDelta-2/pc3/pc1.mma LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/pr3/pr1.ma
 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-2/pc3/subst1.ma LambdaDelta-2/pc3/subst1.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/pr3/subst1.ma
 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/pr2/defs.ma LambdaDelta-2/pr2/defs.mma LambdaDelta-2/getl/defs.ma LambdaDelta-2/pr0/defs.ma
 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-2/csuba/defs.ma LambdaDelta-2/csuba/defs.mma LambdaDelta-2/arity/defs.ma
+LambdaDelta-2/sty1/defs.ma LambdaDelta-2/sty1/defs.mma LambdaDelta-2/sty0/defs.ma
+LambdaDelta-2/sn3/defs.ma LambdaDelta-2/sn3/defs.mma LambdaDelta-2/pr3/defs.ma
+LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pc1/defs.mma LambdaDelta-2/pr1/defs.ma
 LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst0/defs.ma
-Base-2/plist/props.ma Base-2/plist/props.mma
+Base-2/plist/props.ma Base-2/plist/props.mma Base-2/plist/defs.ma
 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/lift1/defs.ma LambdaDelta-2/lift1/defs.mma LambdaDelta-2/lift/defs.ma
 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
+Base-2/ext/tactics.ma Base-2/ext/tactics.mma Base-2/preamble.ma
+LambdaDelta-2/drop1/props.ma LambdaDelta-2/drop1/props.mma LambdaDelta-2/drop/props.ma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/getl/defs.ma
 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-2/ty3/arity.ma LambdaDelta-2/ty3/arity.mma LambdaDelta-2/arity/pr3.ma LambdaDelta-2/asucc/fwd.ma LambdaDelta-2/ty3/pr3_props.ma
 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
@@ -146,7 +146,7 @@ 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/T/dec.ma LambdaDelta-2/T/dec.mma LambdaDelta-2/T/defs.ma
 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
@@ -154,26 +154,26 @@ 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/arity/fwd.ma LambdaDelta-2/arity/fwd.mma LambdaDelta-2/arity/defs.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/leq/asucc.ma
+LambdaDelta-2/app/defs.ma LambdaDelta-2/app/defs.mma LambdaDelta-2/C/defs.ma
 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
+LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/pr0/fwd.mma LambdaDelta-2/pr0/props.ma
 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-2/leq/fwd.ma LambdaDelta-2/leq/fwd.mma LambdaDelta-2/leq/defs.ma
 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
+LambdaDelta-2/drop1/getl.ma LambdaDelta-2/drop1/getl.mma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/getl/drop.ma
 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/clen/getl.ma LambdaDelta-2/clen/getl.mma LambdaDelta-2/clen/defs.ma LambdaDelta-2/getl/props.ma
+LambdaDelta-2/fsubst0/fwd.ma LambdaDelta-2/fsubst0/fwd.mma LambdaDelta-2/fsubst0/defs.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/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
@@ -187,12 +187,12 @@ LambdaDelta-2/nf2/fwd.mma LambdaDelta-1/nf2/fwd.ma LambdaDelta-2/T/props.ma Lamb
 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/ty3.ma LambdaDelta-2/wf3/ty3.mma LambdaDelta-2/wf3/getl.ma
+LambdaDelta-2/ty3/props.ma LambdaDelta-2/ty3/props.mma LambdaDelta-2/pc3/fwd.ma LambdaDelta-2/ty3/fwd.ma
 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
+LambdaDelta-2/wcpr0/defs.ma LambdaDelta-2/wcpr0/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/pr0/defs.ma
 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
@@ -202,22 +202,22 @@ Legacy-2/preamble.ma Legacy-1/preamble.ma Legacy-1/coq/defs.ma Legacy-1/coq/prop
 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/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/tlist/defs.ma LambdaDelta-2/tlist/defs.mma LambdaDelta-2/T/defs.ma
 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/sty0/fwd.ma LambdaDelta-2/sty0/fwd.mma LambdaDelta-2/sty0/defs.ma
 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-2/pr0/pr0.ma LambdaDelta-2/pr0/pr0.mma LambdaDelta-2/lift/tlt.ma LambdaDelta-2/pr0/fwd.ma
 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/iso/fwd.ma LambdaDelta-2/iso/fwd.mma LambdaDelta-2/iso/defs.ma LambdaDelta-2/tlist/defs.ma
+LambdaDelta-2/subst/props.ma LambdaDelta-2/subst/props.mma LambdaDelta-2/lift/props.ma LambdaDelta-2/subst/fwd.ma LambdaDelta-2/subst0/defs.ma
 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
@@ -228,26 +228,26 @@ LambdaDelta-2/pr3/pr3.mma LambdaDelta-1/pr3/pr3.ma LambdaDelta-2/pr2/pr2.ma Lamb
 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-2/wcpr0/fwd.ma LambdaDelta-2/wcpr0/fwd.mma LambdaDelta-2/wcpr0/defs.ma
+LambdaDelta-2/pr0/dec.ma LambdaDelta-2/pr0/dec.mma LambdaDelta-2/T/dec.ma LambdaDelta-2/T/props.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/subst0/dec.ma
+LambdaDelta-2/csubc/getl.ma LambdaDelta-2/csubc/getl.mma LambdaDelta-2/csubc/clear.ma LambdaDelta-2/csubc/drop.ma
 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/arity/pr3.ma LambdaDelta-2/arity/pr3.mma 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/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-2/ex2/defs.ma LambdaDelta-2/ex2/defs.mma LambdaDelta-2/C/defs.ma
+Base-2/ext/arith.ma Base-2/ext/arith.mma Base-2/preamble.ma
 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-2/llt/props.ma LambdaDelta-2/llt/props.mma LambdaDelta-2/leq/defs.ma LambdaDelta-2/llt/defs.ma
 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/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/C/defs.ma LambdaDelta-2/C/defs.mma LambdaDelta-2/T/defs.ma
 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
@@ -255,82 +255,82 @@ LambdaDelta-2/sc3/arity.mma LambdaDelta-1/sc3/arity.ma LambdaDelta-2/csubc/arity
 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/sn3/nf2.ma LambdaDelta-2/sn3/nf2.mma LambdaDelta-2/nf2/dec.ma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/sn3/defs.ma
 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/pr2/fwd.ma LambdaDelta-2/pr2/fwd.mma LambdaDelta-2/getl/clear.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/pr2/defs.ma
 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-2/ty3/nf2.ma LambdaDelta-2/ty3/nf2.mma LambdaDelta-2/nf2/arity.ma LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/ty3/arity.ma
+LambdaDelta-2/pr3/props.ma LambdaDelta-2/pr3/props.mma LambdaDelta-2/pr1/props.ma LambdaDelta-2/pr2/props.ma LambdaDelta-2/pr3/pr1.ma
+LambdaDelta-2/flt/defs.ma LambdaDelta-2/flt/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/getl/defs.ma LambdaDelta-2/getl/defs.mma LambdaDelta-2/clear/defs.ma LambdaDelta-2/drop/defs.ma
+LambdaDelta-2/aprem/defs.ma LambdaDelta-2/aprem/defs.mma LambdaDelta-2/A/defs.ma
+LambdaDelta-2/wf3/clear.ma LambdaDelta-2/wf3/clear.mma LambdaDelta-2/wf3/fwd.ma
 LambdaDelta-1/aplus/defs.ma LambdaDelta-1/asucc/defs.ma
-LambdaDelta-2/clear/fwd.ma LambdaDelta-2/clear/fwd.mma
+LambdaDelta-2/clear/fwd.ma LambdaDelta-2/clear/fwd.mma LambdaDelta-2/clear/defs.ma
 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/csubst0/fwd.ma LambdaDelta-2/csubst0/fwd.mma LambdaDelta-2/csubst0/defs.ma
 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-2/pr2/props.ma LambdaDelta-2/pr2/props.mma LambdaDelta-2/getl/clear.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/pr0/props.ma LambdaDelta-2/pr2/defs.ma
 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-2/arity/defs.ma LambdaDelta-2/arity/defs.mma LambdaDelta-2/getl/defs.ma LambdaDelta-2/leq/defs.ma
+LambdaDelta-2/leq/asucc.ma LambdaDelta-2/leq/asucc.mma LambdaDelta-2/leq/props.ma
 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/subst1/defs.ma LambdaDelta-2/subst1/defs.mma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/pc3/nf2.mma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/pc3/defs.ma
 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-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/csubst0/getl.ma LambdaDelta-2/csubst1/props.ma LambdaDelta-2/drop/props.ma LambdaDelta-2/subst1/props.ma
 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-2/pr3/wcpr0.ma LambdaDelta-2/pr3/wcpr0.mma LambdaDelta-2/pr3/props.ma LambdaDelta-2/wcpr0/getl.ma
 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-2/T/props.ma LambdaDelta-2/T/props.mma LambdaDelta-2/T/defs.ma
 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/ty3/subst1.ma LambdaDelta-2/ty3/subst1.mma LambdaDelta-2/getl/getl.ma LambdaDelta-2/pc3/subst1.ma LambdaDelta-2/ty3/props.ma
+LambdaDelta-2/ty3/defs.ma LambdaDelta-2/ty3/defs.mma LambdaDelta-2/G/defs.ma LambdaDelta-2/pc3/defs.ma
 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-2/csubst0/props.ma LambdaDelta-2/csubst0/props.mma LambdaDelta-2/csubst0/defs.ma
 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-2/pr1/props.ma LambdaDelta-2/pr1/props.mma LambdaDelta-2/T/props.ma LambdaDelta-2/pr0/subst1.ma LambdaDelta-2/pr1/defs.ma LambdaDelta-2/subst1/props.ma
+Base-2/plist/defs.ma Base-2/plist/defs.mma Base-2/preamble.ma
 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/flt/props.ma LambdaDelta-2/flt/props.mma LambdaDelta-2/C/props.ma LambdaDelta-2/flt/defs.ma
 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-2/pr0/defs.ma LambdaDelta-2/pr0/defs.mma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-2/nf2/defs.ma LambdaDelta-2/nf2/defs.mma LambdaDelta-2/pr2/defs.ma
+Base-2/types/props.ma Base-2/types/props.mma Base-2/types/defs.ma
 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/pr3/fwd.ma LambdaDelta-2/pr3/fwd.mma LambdaDelta-2/pr2/fwd.ma LambdaDelta-2/pr3/props.ma
 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/clear/defs.ma LambdaDelta-2/clear/defs.mma LambdaDelta-2/C/defs.ma
 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-2/pr0/props.ma LambdaDelta-2/pr0/props.mma LambdaDelta-2/pr0/defs.ma LambdaDelta-2/subst0/subst0.ma
+LambdaDelta-2/pr3/subst1.ma LambdaDelta-2/pr3/subst1.mma LambdaDelta-2/pr2/subst1.ma LambdaDelta-2/pr3/defs.ma
+LambdaDelta-2/pr2/clen.ma LambdaDelta-2/pr2/clen.mma LambdaDelta-2/clen/getl.ma LambdaDelta-2/pr2/props.ma
 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-2/wf3/defs.ma LambdaDelta-2/wf3/defs.mma LambdaDelta-2/ty3/defs.ma
 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
@@ -338,79 +338,79 @@ 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/csubst1/fwd.ma LambdaDelta-2/csubst1/fwd.mma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/csubst1/defs.ma LambdaDelta-2/subst1/props.ma
+LambdaDelta-2/getl/flt.ma LambdaDelta-2/getl/flt.mma LambdaDelta-2/clear/props.ma LambdaDelta-2/flt/props.ma LambdaDelta-2/getl/fwd.ma
 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-2/getl/props.ma LambdaDelta-2/getl/props.mma LambdaDelta-2/clear/props.ma LambdaDelta-2/drop/props.ma LambdaDelta-2/getl/fwd.ma
+LambdaDelta-2/sc3/defs.ma LambdaDelta-2/sc3/defs.mma LambdaDelta-2/arity/defs.ma LambdaDelta-2/drop1/defs.ma LambdaDelta-2/sn3/defs.ma
 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/llt/defs.ma LambdaDelta-2/llt/defs.mma LambdaDelta-2/A/defs.ma
 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-2/lift1/fwd.ma LambdaDelta-2/lift1/fwd.mma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/lift1/defs.ma
 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/aprem/props.ma LambdaDelta-2/aprem/props.mma LambdaDelta-2/aprem/fwd.ma LambdaDelta-2/leq/defs.ma
 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-2/subst/defs.ma LambdaDelta-2/subst/defs.mma LambdaDelta-2/lift/defs.ma
 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-2/csubc/arity.ma LambdaDelta-2/csubc/arity.mma LambdaDelta-2/csubc/csuba.ma
 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/ex2/props.ma LambdaDelta-2/ex2/props.mma LambdaDelta-2/arity/fwd.ma LambdaDelta-2/ex2/defs.ma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/fwd.ma
+LambdaDelta-2/subst1/subst1.ma LambdaDelta-2/subst1/subst1.mma LambdaDelta-2/subst0/subst0.ma LambdaDelta-2/subst1/fwd.ma
 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
+Legacy-2/coq/props.ma Legacy-2/coq/props.mma Legacy-2/coq/defs.ma
 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
+Base-2/blt/defs.ma Base-2/blt/defs.mma Base-2/preamble.ma
 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.ma LambdaDelta-2/nf2/arity.mma LambdaDelta-2/arity/subst0.ma LambdaDelta-2/nf2/fwd.ma
 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
+LambdaDelta-2/ex1/props.ma LambdaDelta-2/ex1/props.mma 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-2/csubt/ty3.ma LambdaDelta-2/csubt/ty3.mma LambdaDelta-2/csubt/pc3.ma LambdaDelta-2/csubt/props.ma
+LambdaDelta-2/next_plus/props.ma LambdaDelta-2/next_plus/props.mma LambdaDelta-2/next_plus/defs.ma
+LambdaDelta-2/arity/aprem.ma LambdaDelta-2/arity/aprem.mma LambdaDelta-2/aprem/props.ma LambdaDelta-2/arity/cimp.ma LambdaDelta-2/arity/props.ma
 Legacy-2/theory.ma Legacy-2/coq/props.ma
-LambdaDelta-2/drop/fwd.ma LambdaDelta-2/drop/fwd.mma
+LambdaDelta-2/drop/fwd.ma LambdaDelta-2/drop/fwd.mma LambdaDelta-2/drop/defs.ma
 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
+LambdaDelta-2/csuba/arity.ma LambdaDelta-2/csuba/arity.mma LambdaDelta-2/arity/props.ma LambdaDelta-2/csuba/getl.ma LambdaDelta-2/csuba/props.ma LambdaDelta-2/csubv/getl.ma
+LambdaDelta-2/ex0/props.ma LambdaDelta-2/ex0/props.mma LambdaDelta-2/aplus/props.ma LambdaDelta-2/ex0/defs.ma LambdaDelta-2/leq/defs.ma
 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/sty1/props.ma LambdaDelta-2/sty1/props.mma LambdaDelta-2/sty0/props.ma LambdaDelta-2/sty1/defs.ma
+LambdaDelta-2/pr3/defs.ma LambdaDelta-2/pr3/defs.mma LambdaDelta-2/pr2/defs.ma
+LambdaDelta-2/pr3/pr3.ma LambdaDelta-2/pr3/pr3.mma LambdaDelta-2/pr2/pr2.ma LambdaDelta-2/pr3/props.ma
+LambdaDelta-2/csubv/clear.ma LambdaDelta-2/csubv/clear.mma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/csubv/defs.ma
 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-2/csubc/props.ma LambdaDelta-2/csubc/props.mma LambdaDelta-2/csubc/defs.ma LambdaDelta-2/sc3/props.ma
 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/nf2/props.ma LambdaDelta-2/nf2/props.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/fwd.ma
+LambdaDelta-2/leq/defs.ma LambdaDelta-2/leq/defs.mma LambdaDelta-2/aplus/defs.ma
 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/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/sty0/props.ma LambdaDelta-2/sty0/props.mma LambdaDelta-2/getl/drop.ma LambdaDelta-2/sty0/defs.ma
 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
@@ -418,114 +418,114 @@ LambdaDelta-2/subst0/props.mma LambdaDelta-1/subst0/props.ma LambdaDelta-2/subst
 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-2/csuba/getl.ma LambdaDelta-2/csuba/getl.mma LambdaDelta-2/csuba/clear.ma LambdaDelta-2/csuba/drop.ma LambdaDelta-2/getl/clear.ma
 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-2/T/defs.ma LambdaDelta-2/T/defs.mma LambdaDelta-2/preamble.ma
 LambdaDelta-1/tlist/defs.ma LambdaDelta-1/T/defs.ma
-Base-2/blt/props.ma Base-2/blt/props.mma
+LambdaDelta-2/lift/tlt.ma LambdaDelta-2/lift/tlt.mma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/tlt/props.ma
+Base-2/blt/props.ma Base-2/blt/props.mma Base-2/blt/defs.ma
 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-2/csubv/drop.ma LambdaDelta-2/csubv/drop.mma LambdaDelta-2/csubv/props.ma LambdaDelta-2/drop/fwd.ma
 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/ex0/defs.ma LambdaDelta-2/ex0/defs.mma LambdaDelta-2/A/defs.ma LambdaDelta-2/G/defs.ma
 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
+Legacy-2/coq/defs.ma Legacy-2/coq/defs.mma Legacy-2/preamble.ma
+LambdaDelta-2/aprem/fwd.ma LambdaDelta-2/aprem/fwd.mma LambdaDelta-2/aprem/defs.ma
 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-2/csubt/clear.ma LambdaDelta-2/csubt/clear.mma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/csubt/defs.ma
 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-2/csuba/props.ma LambdaDelta-2/csuba/props.mma LambdaDelta-2/csuba/defs.ma
+LambdaDelta-2/next_plus/defs.ma LambdaDelta-2/next_plus/defs.mma LambdaDelta-2/G/defs.ma
 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/r/defs.ma LambdaDelta-2/r/defs.mma LambdaDelta-2/T/defs.ma
 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-2/asucc/fwd.ma LambdaDelta-2/asucc/fwd.mma LambdaDelta-2/asucc/defs.ma
+LambdaDelta-2/tlt/defs.ma LambdaDelta-2/tlt/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/arity/cimp.ma LambdaDelta-2/arity/cimp.mma LambdaDelta-2/arity/defs.ma LambdaDelta-2/cimp/props.ma
 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-2/A/defs.ma LambdaDelta-2/A/defs.mma LambdaDelta-2/preamble.ma
+LambdaDelta-2/csubt/csuba.ma LambdaDelta-2/csubt/csuba.mma LambdaDelta-2/ty3/arity.ma
 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/pc3/props.ma LambdaDelta-2/pc3/props.mma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/pr3/pr3.ma
 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-2/csubc/drop.ma LambdaDelta-2/csubc/drop.mma LambdaDelta-2/csubc/fwd.ma LambdaDelta-2/sc3/props.ma
 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-2/iso/props.ma LambdaDelta-2/iso/props.mma LambdaDelta-2/iso/fwd.ma
 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/tlist/props.ma LambdaDelta-2/tlist/props.mma LambdaDelta-2/tlist/defs.ma
 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/clear/props.ma LambdaDelta-2/clear/props.mma LambdaDelta-2/clear/fwd.ma
+LambdaDelta-2/subst0/subst0.ma LambdaDelta-2/subst0/subst0.mma LambdaDelta-2/subst0/props.ma
+LambdaDelta-2/s/props.ma LambdaDelta-2/s/props.mma LambdaDelta-2/s/defs.ma
+LambdaDelta-2/csubst0/defs.ma LambdaDelta-2/csubst0/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/subst0/defs.ma
 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/r/props.ma LambdaDelta-2/r/props.mma LambdaDelta-2/r/defs.ma LambdaDelta-2/s/defs.ma
 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/pc3/wcpr0.ma LambdaDelta-2/pc3/wcpr0.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/wcpr0/getl.ma
+LambdaDelta-2/arity/props.ma LambdaDelta-2/arity/props.mma LambdaDelta-2/arity/fwd.ma
 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
+LambdaDelta-2/wcpr0/getl.ma LambdaDelta-2/wcpr0/getl.mma LambdaDelta-2/getl/props.ma LambdaDelta-2/wcpr0/defs.ma
+LambdaDelta-2/pc1/props.ma LambdaDelta-2/pc1/props.mma LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pr1/pr1.ma
 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/aplus/props.ma LambdaDelta-2/aplus/props.mma LambdaDelta-2/aplus/defs.ma LambdaDelta-2/next_plus/props.ma
 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/pr1/pr1.ma LambdaDelta-2/pr1/pr1.mma LambdaDelta-2/pr0/pr0.ma LambdaDelta-2/pr1/props.ma
 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-2/pc3/left.ma LambdaDelta-2/pc3/left.mma LambdaDelta-2/pc3/props.ma
 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/nf2/iso.ma LambdaDelta-2/nf2/iso.mma LambdaDelta-2/iso/props.ma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/pr3/fwd.ma
 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-2/fsubst0/defs.ma LambdaDelta-2/fsubst0/defs.mma LambdaDelta-2/csubst0/defs.ma
 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-2/csuba/fwd.ma LambdaDelta-2/csuba/fwd.mma LambdaDelta-2/csuba/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/subst0/tlt.ma LambdaDelta-2/subst0/tlt.mma LambdaDelta-2/lift/props.ma LambdaDelta-2/lift/tlt.ma LambdaDelta-2/subst0/defs.ma
 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-2/sn3/props.ma LambdaDelta-2/sn3/props.mma LambdaDelta-2/nf2/iso.ma LambdaDelta-2/pr3/iso.ma LambdaDelta-2/sn3/fwd.ma LambdaDelta-2/sn3/nf2.ma
 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
@@ -533,128 +533,128 @@ LambdaDelta-1/getl/props.ma LambdaDelta-1/clear/props.ma LambdaDelta-1/drop/prop
 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-2/asucc/defs.ma LambdaDelta-2/asucc/defs.mma LambdaDelta-2/A/defs.ma LambdaDelta-2/G/defs.ma
 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-2/getl/getl.ma LambdaDelta-2/getl/getl.mma LambdaDelta-2/getl/clear.ma LambdaDelta-2/getl/drop.ma
 LambdaDelta-1/next_plus/defs.ma LambdaDelta-1/G/defs.ma
-LambdaDelta-2/cimp/props.ma LambdaDelta-2/cimp/props.mma
+LambdaDelta-2/cimp/props.ma LambdaDelta-2/cimp/props.mma LambdaDelta-2/cimp/defs.ma LambdaDelta-2/getl/getl.ma
 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/lift1/props.ma LambdaDelta-2/lift1/props.mma LambdaDelta-2/drop1/defs.ma LambdaDelta-2/lift/props.ma
+LambdaDelta-2/cnt/defs.ma LambdaDelta-2/cnt/defs.mma LambdaDelta-2/T/defs.ma
 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/subst1/props.ma LambdaDelta-2/subst1/props.mma LambdaDelta-2/subst0/props.ma LambdaDelta-2/subst1/defs.ma
+LambdaDelta-2/leq/props.ma LambdaDelta-2/leq/props.mma LambdaDelta-2/aplus/props.ma LambdaDelta-2/leq/fwd.ma
+LambdaDelta-2/pr1/defs.ma LambdaDelta-2/pr1/defs.mma LambdaDelta-2/pr0/defs.ma
 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/arity/subst0.ma LambdaDelta-2/arity/subst0.mma 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/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-2/sty0/defs.ma LambdaDelta-2/sty0/defs.mma LambdaDelta-2/G/defs.ma LambdaDelta-2/getl/defs.ma
 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-2/subst0/props.ma LambdaDelta-2/subst0/props.mma LambdaDelta-2/subst0/fwd.ma
 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-2/G/defs.ma LambdaDelta-2/G/defs.mma LambdaDelta-2/preamble.ma
 LambdaDelta-1/subst0/defs.ma LambdaDelta-1/lift/defs.ma
-LambdaDelta-2/cimp/defs.ma LambdaDelta-2/cimp/defs.mma
+LambdaDelta-2/cimp/defs.ma LambdaDelta-2/cimp/defs.mma LambdaDelta-2/getl/defs.ma
 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/lift/defs.ma LambdaDelta-2/lift/defs.mma LambdaDelta-2/s/defs.ma LambdaDelta-2/tlist/defs.ma
+LambdaDelta-2/drop1/defs.ma LambdaDelta-2/drop1/defs.mma LambdaDelta-2/drop/defs.ma LambdaDelta-2/lift1/defs.ma
 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/C/props.ma LambdaDelta-2/C/props.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/T/props.ma
 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-2/clen/defs.ma LambdaDelta-2/clen/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/s/defs.ma
 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/sty1/cnt.ma LambdaDelta-2/sty1/cnt.mma LambdaDelta-2/cnt/props.ma LambdaDelta-2/sty1/props.ma
+LambdaDelta-2/pr3/pr1.ma LambdaDelta-2/pr3/pr1.mma LambdaDelta-2/pr1/defs.ma LambdaDelta-2/pr3/defs.ma
 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-2/wf3/getl.ma LambdaDelta-2/wf3/getl.mma LambdaDelta-2/ty3/dec.ma LambdaDelta-2/wf3/clear.ma
+LambdaDelta-2/wf3/fwd.ma LambdaDelta-2/wf3/fwd.mma LambdaDelta-2/wf3/defs.ma
 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-2/csubt/drop.ma LambdaDelta-2/csubt/drop.mma LambdaDelta-2/csubt/fwd.ma LambdaDelta-2/drop/fwd.ma
 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-2/nf2/lift1.ma LambdaDelta-2/nf2/lift1.mma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/nf2/props.ma
 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-2/drop1/fwd.ma LambdaDelta-2/drop1/fwd.mma LambdaDelta-2/drop1/defs.ma
+LambdaDelta-2/csubc/fwd.ma LambdaDelta-2/csubc/fwd.mma LambdaDelta-2/csubc/defs.ma
 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/lift/fwd.ma LambdaDelta-2/lift/fwd.mma LambdaDelta-2/lift/defs.ma
 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-2/csubv/defs.ma LambdaDelta-2/csubv/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/csuba/drop.ma LambdaDelta-2/csuba/drop.mma LambdaDelta-2/csuba/fwd.ma LambdaDelta-2/drop/fwd.ma
 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-2/ty3/fsubst0.ma LambdaDelta-2/ty3/fsubst0.mma LambdaDelta-2/getl/getl.ma LambdaDelta-2/pc3/fsubst0.ma LambdaDelta-2/ty3/props.ma
+LambdaDelta-2/sn3/fwd.ma LambdaDelta-2/sn3/fwd.mma LambdaDelta-2/pr3/props.ma LambdaDelta-2/sn3/defs.ma
 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/tlt/props.ma LambdaDelta-2/tlt/props.mma LambdaDelta-2/tlt/defs.ma
 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/pr0/subst1.ma LambdaDelta-2/pr0/subst1.mma LambdaDelta-2/pr0/props.ma LambdaDelta-2/subst1/defs.ma
 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/wf3/props.ma LambdaDelta-2/wf3/props.mma LambdaDelta-2/app/defs.ma LambdaDelta-2/wf3/ty3.ma
 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-2/csubst0/clear.ma LambdaDelta-2/csubst0/clear.mma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/csubst0/props.ma
 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
+Base-2/types/defs.ma Base-2/types/defs.mma Base-2/preamble.ma
 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/ty3/fwd.ma LambdaDelta-2/ty3/fwd.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/ty3/defs.ma
 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/csubc/defs.ma LambdaDelta-2/csubc/defs.mma LambdaDelta-2/sc3/defs.ma
 LambdaDelta-2/csubt/defs.mma LambdaDelta-2/ty3/defs.ma
-LambdaDelta-2/iso/defs.ma LambdaDelta-2/iso/defs.mma
+LambdaDelta-2/iso/defs.ma LambdaDelta-2/iso/defs.mma LambdaDelta-2/T/defs.ma
 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/pc3/defs.ma LambdaDelta-2/pc3/defs.mma LambdaDelta-2/pr3/defs.ma
 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
@@ -662,34 +662,34 @@ LambdaDelta-1/ex0/props.ma LambdaDelta-1/aplus/props.ma LambdaDelta-1/ex0/defs.m
 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/pr2/subst1.ma LambdaDelta-2/pr2/subst1.mma 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-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-2/pc3/fwd.ma LambdaDelta-2/pc3/fwd.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/pr3/fwd.ma
 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/drop1.ma LambdaDelta-2/csubc/drop1.mma LambdaDelta-2/csubc/drop.ma
 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-2/getl/clear.ma LambdaDelta-2/getl/clear.mma LambdaDelta-2/clear/drop.ma LambdaDelta-2/getl/props.ma
 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/getl/fwd.ma LambdaDelta-2/getl/fwd.mma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/getl/defs.ma
 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/ex1/defs.ma LambdaDelta-2/ex1/defs.mma LambdaDelta-2/C/defs.ma
 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/subst/fwd.ma LambdaDelta-2/subst/fwd.mma LambdaDelta-2/subst/defs.ma
 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/s/defs.ma LambdaDelta-2/s/defs.mma LambdaDelta-2/T/defs.ma
 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
+LambdaDelta-2/ty3/arity_props.ma LambdaDelta-2/ty3/arity_props.mma LambdaDelta-2/sc3/arity.ma LambdaDelta-2/ty3/arity.ma
 Base-1/plist/props.ma Base-1/plist/defs.ma
-LambdaDelta-2/arity/lift1.ma LambdaDelta-2/arity/lift1.mma
+LambdaDelta-2/arity/lift1.ma LambdaDelta-2/arity/lift1.mma LambdaDelta-2/arity/props.ma LambdaDelta-2/drop1/fwd.ma
 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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 99c132c11d27cf2a6f951ef71087bc26aadaf172..9c331d2ee2da2bf2a0bc9d692aa9c58543c4f451 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -373,7 +373,11 @@ module F =
           let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
          let atexit = dump generated in
          let res = compile options fname in
-         atexit res
+         let r = atexit res in
+         if r then r else begin
+            Sys.remove generated;
+            Printf.printf "rm %s\n" generated; flush stdout; r
+         end
        else
           compile options fname