+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/preamble.ma
+LambdaDelta-1/tlist/defs.ma LambdaDelta-1/T/defs.ma
+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/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/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 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/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/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/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/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/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/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/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/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/defs.ma
+LambdaDelta-2/subst0/defs.mma LambdaDelta-2/lift/defs.ma
+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/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/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/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/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/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