helm/software/matita/contribs/LAMBDA-TYPES/depends

   1 Legacy-2/preamble.ma Legacy-1/coq/defs.ma Legacy-1/coq/props.ma Legacy-1/definitions.ma Legacy-1/preamble.ma
   2 Legacy-2/coq/defs.ma Legacy-2/preamble.ma
   3 Legacy-2/coq/props.ma Legacy-2/coq/defs.ma
   4 LambdaDelta-1/spare.ma LambdaDelta-1/theory.ma
   5 LambdaDelta-1/preamble.ma Base-1/theory.ma
   6 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
   7 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
   8 LambdaDelta-1/csubv/props.ma LambdaDelta-1/T/props.ma LambdaDelta-1/csubv/defs.ma
   9 LambdaDelta-1/csubv/drop.ma LambdaDelta-1/csubv/props.ma LambdaDelta-1/drop/fwd.ma
  10 LambdaDelta-1/csubv/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubv/defs.ma
  11 LambdaDelta-1/csubv/getl.ma LambdaDelta-1/csubv/clear.ma LambdaDelta-1/csubv/drop.ma LambdaDelta-1/getl/fwd.ma
  12 LambdaDelta-1/csubv/defs.ma LambdaDelta-1/C/defs.ma
  13 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
  14 LambdaDelta-1/ex2/defs.ma LambdaDelta-1/C/defs.ma
  15 LambdaDelta-1/tlist/props.ma LambdaDelta-1/tlist/defs.ma
  16 LambdaDelta-1/tlist/defs.ma LambdaDelta-1/T/defs.ma
  17 LambdaDelta-1/clen/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/s/defs.ma
  18 LambdaDelta-1/clen/getl.ma LambdaDelta-1/clen/defs.ma LambdaDelta-1/getl/props.ma
  19 LambdaDelta-1/leq/props.ma LambdaDelta-1/aplus/props.ma LambdaDelta-1/leq/fwd.ma
  20 LambdaDelta-1/leq/asucc.ma LambdaDelta-1/leq/props.ma
  21 LambdaDelta-1/leq/defs.ma LambdaDelta-1/aplus/defs.ma
  22 LambdaDelta-1/leq/fwd.ma LambdaDelta-1/leq/defs.ma
  23 LambdaDelta-1/pr3/props.ma LambdaDelta-1/pr1/props.ma LambdaDelta-1/pr2/props.ma LambdaDelta-1/pr3/pr1.ma
  24 LambdaDelta-1/pr3/pr3.ma LambdaDelta-1/pr2/pr2.ma LambdaDelta-1/pr3/props.ma
  25 LambdaDelta-1/pr3/defs.ma LambdaDelta-1/pr2/defs.ma
  26 LambdaDelta-1/pr3/fwd.ma LambdaDelta-1/pr2/fwd.ma LambdaDelta-1/pr3/props.ma
  27 LambdaDelta-1/pr3/subst1.ma LambdaDelta-1/pr2/subst1.ma LambdaDelta-1/pr3/defs.ma
  28 LambdaDelta-1/pr3/iso.ma LambdaDelta-1/iso/props.ma LambdaDelta-1/pr3/fwd.ma LambdaDelta-1/tlist/props.ma
  29 LambdaDelta-1/pr3/wcpr0.ma LambdaDelta-1/pr3/props.ma LambdaDelta-1/wcpr0/getl.ma
  30 LambdaDelta-1/pr3/pr1.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr3/defs.ma
  31 LambdaDelta-1/ty3/fsubst0.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/pc3/fsubst0.ma LambdaDelta-1/ty3/props.ma
  32 LambdaDelta-1/ty3/props.ma LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/ty3/fwd.ma
  33 LambdaDelta-1/ty3/arity_props.ma LambdaDelta-1/sc3/arity.ma LambdaDelta-1/ty3/arity.ma
  34 LambdaDelta-1/ty3/arity.ma LambdaDelta-1/arity/pr3.ma LambdaDelta-1/asucc/fwd.ma LambdaDelta-1/ty3/pr3_props.ma
  35 LambdaDelta-1/ty3/pr3_props.ma LambdaDelta-1/ty3/pr3.ma
  36 LambdaDelta-1/ty3/sty0.ma LambdaDelta-1/sty0/fwd.ma LambdaDelta-1/ty3/pr3_props.ma
  37 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
  38 LambdaDelta-1/ty3/defs.ma LambdaDelta-1/G/defs.ma LambdaDelta-1/pc3/defs.ma
  39 LambdaDelta-1/ty3/fwd.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/ty3/defs.ma
  40 LambdaDelta-1/ty3/dec.ma LambdaDelta-1/getl/dec.ma LambdaDelta-1/getl/flt.ma LambdaDelta-1/pc3/dec.ma
  41 LambdaDelta-1/ty3/subst1.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/pc3/subst1.ma LambdaDelta-1/ty3/props.ma
  42 LambdaDelta-1/ty3/nf2.ma LambdaDelta-1/nf2/arity.ma LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/ty3/arity.ma
  43 LambdaDelta-1/ty3/fwd_nf2.ma LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/ty3/arity_props.ma
  44 LambdaDelta-1/cnt/props.ma LambdaDelta-1/cnt/defs.ma LambdaDelta-1/lift/fwd.ma
  45 LambdaDelta-1/cnt/defs.ma LambdaDelta-1/T/defs.ma
  46 LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/csubst0/defs.ma
  47 LambdaDelta-1/fsubst0/fwd.ma LambdaDelta-1/fsubst0/defs.ma
  48 LambdaDelta-1/iso/props.ma LambdaDelta-1/iso/fwd.ma
  49 LambdaDelta-1/iso/defs.ma LambdaDelta-1/T/defs.ma
  50 LambdaDelta-1/iso/fwd.ma LambdaDelta-1/iso/defs.ma LambdaDelta-1/tlist/defs.ma
  51 LambdaDelta-1/lift/props.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/s/props.ma
  52 LambdaDelta-1/lift/defs.ma LambdaDelta-1/s/defs.ma LambdaDelta-1/tlist/defs.ma
  53 LambdaDelta-1/lift/tlt.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/tlt/props.ma
  54 LambdaDelta-1/lift/fwd.ma LambdaDelta-1/lift/defs.ma
  55 LambdaDelta-1/flt/props.ma LambdaDelta-1/C/props.ma LambdaDelta-1/flt/defs.ma
  56 LambdaDelta-1/flt/defs.ma LambdaDelta-1/C/defs.ma
  57 LambdaDelta-1/A/defs.ma LambdaDelta-1/preamble.ma
  58 LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst0/fwd.ma
  59 LambdaDelta-1/subst0/defs.ma LambdaDelta-1/lift/defs.ma
  60 LambdaDelta-1/subst0/tlt.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/lift/tlt.ma LambdaDelta-1/subst0/defs.ma
  61 LambdaDelta-1/subst0/fwd.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst0/defs.ma
  62 LambdaDelta-1/subst0/subst0.ma LambdaDelta-1/subst0/props.ma
  63 LambdaDelta-1/subst0/dec.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst0/defs.ma
  64 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
  65 LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr0/defs.ma
  66 LambdaDelta-1/pr1/pr1.ma LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/pr1/props.ma
  67 LambdaDelta-1/T/props.ma LambdaDelta-1/T/defs.ma
  68 LambdaDelta-1/T/defs.ma LambdaDelta-1/preamble.ma
  69 LambdaDelta-1/T/dec.ma LambdaDelta-1/T/defs.ma
  70 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
  71 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
  72 LambdaDelta-1/sc3/defs.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/sn3/defs.ma
  73 LambdaDelta-1/aplus/props.ma LambdaDelta-1/aplus/defs.ma LambdaDelta-1/next_plus/props.ma
  74 LambdaDelta-1/aplus/defs.ma LambdaDelta-1/asucc/defs.ma
  75 LambdaDelta-1/asucc/defs.ma LambdaDelta-1/A/defs.ma LambdaDelta-1/G/defs.ma
  76 LambdaDelta-1/asucc/fwd.ma LambdaDelta-1/asucc/defs.ma
  77 LambdaDelta-1/aprem/props.ma LambdaDelta-1/aprem/fwd.ma LambdaDelta-1/leq/defs.ma
  78 LambdaDelta-1/aprem/defs.ma LambdaDelta-1/A/defs.ma
  79 LambdaDelta-1/aprem/fwd.ma LambdaDelta-1/aprem/defs.ma
  80 LambdaDelta-1/nf2/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/fwd.ma
  81 LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr3/pr3.ma
  82 LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/defs.ma
  83 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
  84 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
  85 LambdaDelta-1/nf2/lift1.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/nf2/props.ma
  86 LambdaDelta-1/nf2/iso.ma LambdaDelta-1/iso/props.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/pr3/fwd.ma
  87 LambdaDelta-1/nf2/arity.ma LambdaDelta-1/arity/subst0.ma LambdaDelta-1/nf2/fwd.ma
  88 LambdaDelta-1/drop/props.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/r/props.ma
  89 LambdaDelta-1/drop/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/lift/defs.ma LambdaDelta-1/r/defs.ma
  90 LambdaDelta-1/drop/fwd.ma LambdaDelta-1/drop/defs.ma
  91 LambdaDelta-1/csuba/drop.ma LambdaDelta-1/csuba/fwd.ma LambdaDelta-1/drop/fwd.ma
  92 LambdaDelta-1/csuba/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csuba/defs.ma
  93 LambdaDelta-1/csuba/props.ma LambdaDelta-1/csuba/defs.ma
  94 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
  95 LambdaDelta-1/csuba/defs.ma LambdaDelta-1/arity/defs.ma
  96 LambdaDelta-1/csuba/fwd.ma LambdaDelta-1/csuba/defs.ma
  97 LambdaDelta-1/csuba/getl.ma LambdaDelta-1/csuba/clear.ma LambdaDelta-1/csuba/drop.ma LambdaDelta-1/getl/clear.ma
  98 LambdaDelta-1/C/props.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/T/props.ma
  99 LambdaDelta-1/C/defs.ma LambdaDelta-1/T/defs.ma
 100 LambdaDelta-1/csubt/drop.ma LambdaDelta-1/csubt/fwd.ma LambdaDelta-1/drop/fwd.ma
 101 LambdaDelta-1/csubt/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubt/defs.ma
 102 LambdaDelta-1/csubt/props.ma LambdaDelta-1/csubt/defs.ma
 103 LambdaDelta-1/csubt/pc3.ma LambdaDelta-1/csubt/getl.ma LambdaDelta-1/pc3/left.ma
 104 LambdaDelta-1/csubt/defs.ma LambdaDelta-1/ty3/defs.ma
 105 LambdaDelta-1/csubt/fwd.ma LambdaDelta-1/csubt/defs.ma
 106 LambdaDelta-1/csubt/ty3.ma LambdaDelta-1/csubt/pc3.ma LambdaDelta-1/csubt/props.ma
 107 LambdaDelta-1/csubt/getl.ma LambdaDelta-1/csubt/clear.ma LambdaDelta-1/csubt/drop.ma LambdaDelta-1/getl/clear.ma
 108 LambdaDelta-1/csubt/csuba.ma LambdaDelta-1/ty3/arity.ma
 109 LambdaDelta-1/cimp/props.ma LambdaDelta-1/cimp/defs.ma LambdaDelta-1/getl/getl.ma
 110 LambdaDelta-1/cimp/defs.ma LambdaDelta-1/getl/defs.ma
 111 LambdaDelta-1/drop1/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/getl/defs.ma
 112 LambdaDelta-1/drop1/defs.ma LambdaDelta-1/drop/defs.ma LambdaDelta-1/lift1/defs.ma
 113 LambdaDelta-1/drop1/getl.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/getl/drop.ma
 114 LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/drop1/defs.ma
 115 LambdaDelta-1/lift1/props.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/lift/props.ma
 116 LambdaDelta-1/lift1/defs.ma LambdaDelta-1/lift/defs.ma
 117 LambdaDelta-1/lift1/fwd.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/lift1/defs.ma
 118 LambdaDelta-1/pr2/pr2.ma LambdaDelta-1/getl/props.ma LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/pr2/defs.ma
 119 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
 120 LambdaDelta-1/pr2/defs.ma LambdaDelta-1/getl/defs.ma LambdaDelta-1/pr0/defs.ma
 121 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
 122 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
 123 LambdaDelta-1/pr2/clen.ma LambdaDelta-1/clen/getl.ma LambdaDelta-1/pr2/props.ma
 124 LambdaDelta-1/pc3/fsubst0.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/pc3/left.ma
 125 LambdaDelta-1/pc3/pc1.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/pr1.ma
 126 LambdaDelta-1/pc3/props.ma LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/pr3.ma
 127 LambdaDelta-1/pc3/left.ma LambdaDelta-1/pc3/props.ma
 128 LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/defs.ma
 129 LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/pr3/fwd.ma
 130 LambdaDelta-1/pc3/dec.ma LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/ty3/arity_props.ma
 131 LambdaDelta-1/pc3/subst1.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/pr3/subst1.ma
 132 LambdaDelta-1/pc3/wcpr0.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/wcpr0/getl.ma
 133 LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/pc3/defs.ma
 134 LambdaDelta-1/pr0/props.ma LambdaDelta-1/pr0/defs.ma LambdaDelta-1/subst0/subst0.ma
 135 LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/lift/tlt.ma LambdaDelta-1/pr0/fwd.ma
 136 LambdaDelta-1/pr0/defs.ma LambdaDelta-1/subst0/defs.ma
 137 LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr0/props.ma
 138 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
 139 LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr0/props.ma LambdaDelta-1/subst1/defs.ma
 140 LambdaDelta-1/subst1/props.ma LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst1/defs.ma
 141 LambdaDelta-1/subst1/defs.ma LambdaDelta-1/subst0/defs.ma
 142 LambdaDelta-1/subst1/fwd.ma LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst1/defs.ma
 143 LambdaDelta-1/subst1/subst1.ma LambdaDelta-1/subst0/subst0.ma LambdaDelta-1/subst1/fwd.ma
 144 LambdaDelta-1/tlt/props.ma LambdaDelta-1/tlt/defs.ma
 145 LambdaDelta-1/tlt/defs.ma LambdaDelta-1/T/defs.ma
 146 LambdaDelta-1/ex0/props.ma LambdaDelta-1/aplus/props.ma LambdaDelta-1/ex0/defs.ma LambdaDelta-1/leq/defs.ma
 147 LambdaDelta-1/ex0/defs.ma LambdaDelta-1/A/defs.ma LambdaDelta-1/G/defs.ma
 148 LambdaDelta-1/r/props.ma LambdaDelta-1/r/defs.ma LambdaDelta-1/s/defs.ma
 149 LambdaDelta-1/r/defs.ma LambdaDelta-1/T/defs.ma
 150 LambdaDelta-1/wcpr0/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/pr0/defs.ma
 151 LambdaDelta-1/wcpr0/fwd.ma LambdaDelta-1/wcpr0/defs.ma
 152 LambdaDelta-1/wcpr0/getl.ma LambdaDelta-1/getl/props.ma LambdaDelta-1/wcpr0/defs.ma
 153 LambdaDelta-1/G/defs.ma LambdaDelta-1/preamble.ma
 154 LambdaDelta-1/csubst0/drop.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/s/props.ma
 155 LambdaDelta-1/csubst0/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst0/props.ma
 156 LambdaDelta-1/csubst0/props.ma LambdaDelta-1/csubst0/defs.ma
 157 LambdaDelta-1/csubst0/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/subst0/defs.ma
 158 LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst0/defs.ma
 159 LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/csubst0/clear.ma LambdaDelta-1/csubst0/drop.ma LambdaDelta-1/getl/fwd.ma
 160 LambdaDelta-1/next_plus/props.ma LambdaDelta-1/next_plus/defs.ma
 161 LambdaDelta-1/next_plus/defs.ma LambdaDelta-1/G/defs.ma
 162 LambdaDelta-1/csubc/drop.ma LambdaDelta-1/csubc/fwd.ma LambdaDelta-1/sc3/props.ma
 163 LambdaDelta-1/csubc/clear.ma LambdaDelta-1/csubc/fwd.ma
 164 LambdaDelta-1/csubc/props.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/props.ma
 165 LambdaDelta-1/csubc/arity.ma LambdaDelta-1/csubc/csuba.ma
 166 LambdaDelta-1/csubc/drop1.ma LambdaDelta-1/csubc/drop.ma
 167 LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/defs.ma
 168 LambdaDelta-1/csubc/csuba.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/props.ma
 169 LambdaDelta-1/csubc/getl.ma LambdaDelta-1/csubc/clear.ma LambdaDelta-1/csubc/drop.ma
 170 LambdaDelta-1/csubc/fwd.ma LambdaDelta-1/csubc/defs.ma
 171 LambdaDelta-1/arity/props.ma LambdaDelta-1/arity/fwd.ma
 172 LambdaDelta-1/arity/aprem.ma LambdaDelta-1/aprem/props.ma LambdaDelta-1/arity/cimp.ma LambdaDelta-1/arity/props.ma
 173 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
 174 LambdaDelta-1/arity/defs.ma LambdaDelta-1/getl/defs.ma LambdaDelta-1/leq/defs.ma
 175 LambdaDelta-1/arity/fwd.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/leq/asucc.ma
 176 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
 177 LambdaDelta-1/arity/lift1.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/drop1/fwd.ma
 178 LambdaDelta-1/arity/cimp.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/cimp/props.ma
 179 LambdaDelta-1/subst/props.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst/fwd.ma LambdaDelta-1/subst0/defs.ma
 180 LambdaDelta-1/subst/fwd.ma LambdaDelta-1/subst/defs.ma
 181 LambdaDelta-1/subst/defs.ma LambdaDelta-1/lift/defs.ma
 182 LambdaDelta-1/getl/drop.ma LambdaDelta-1/clear/drop.ma LambdaDelta-1/getl/props.ma
 183 LambdaDelta-1/getl/clear.ma LambdaDelta-1/clear/drop.ma LambdaDelta-1/getl/props.ma
 184 LambdaDelta-1/getl/props.ma LambdaDelta-1/clear/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/getl/fwd.ma
 185 LambdaDelta-1/getl/defs.ma LambdaDelta-1/clear/defs.ma LambdaDelta-1/drop/defs.ma
 186 LambdaDelta-1/getl/fwd.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/getl/defs.ma
 187 LambdaDelta-1/getl/dec.ma LambdaDelta-1/getl/props.ma
 188 LambdaDelta-1/getl/flt.ma LambdaDelta-1/clear/props.ma LambdaDelta-1/flt/props.ma LambdaDelta-1/getl/fwd.ma
 189 LambdaDelta-1/getl/getl.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma
 190 LambdaDelta-1/clear/drop.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/drop/fwd.ma
 191 LambdaDelta-1/clear/props.ma LambdaDelta-1/clear/fwd.ma
 192 LambdaDelta-1/clear/defs.ma LambdaDelta-1/C/defs.ma
 193 LambdaDelta-1/clear/fwd.ma LambdaDelta-1/clear/defs.ma
 194 LambdaDelta-1/sty1/props.ma LambdaDelta-1/sty0/props.ma LambdaDelta-1/sty1/defs.ma
 195 LambdaDelta-1/sty1/cnt.ma LambdaDelta-1/cnt/props.ma LambdaDelta-1/sty1/props.ma
 196 LambdaDelta-1/sty1/defs.ma LambdaDelta-1/sty0/defs.ma
 197 LambdaDelta-1/s/props.ma LambdaDelta-1/s/defs.ma
 198 LambdaDelta-1/s/defs.ma LambdaDelta-1/T/defs.ma
 199 LambdaDelta-1/pc1/props.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pr1/pr1.ma
 200 LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pr1/defs.ma
 201 LambdaDelta-1/wf3/props.ma LambdaDelta-1/app/defs.ma LambdaDelta-1/wf3/ty3.ma
 202 LambdaDelta-1/wf3/clear.ma LambdaDelta-1/wf3/fwd.ma
 203 LambdaDelta-1/wf3/getl.ma LambdaDelta-1/ty3/dec.ma LambdaDelta-1/wf3/clear.ma
 204 LambdaDelta-1/wf3/ty3.ma LambdaDelta-1/wf3/getl.ma
 205 LambdaDelta-1/wf3/fwd.ma LambdaDelta-1/wf3/defs.ma
 206 LambdaDelta-1/wf3/defs.ma LambdaDelta-1/ty3/defs.ma
 207 LambdaDelta-1/sty0/props.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/sty0/defs.ma
 208 LambdaDelta-1/sty0/fwd.ma LambdaDelta-1/sty0/defs.ma
 209 LambdaDelta-1/sty0/defs.ma LambdaDelta-1/G/defs.ma LambdaDelta-1/getl/defs.ma
 210 LambdaDelta-1/app/defs.ma LambdaDelta-1/C/defs.ma
 211 LambdaDelta-1/sn3/nf2.ma LambdaDelta-1/nf2/dec.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/sn3/defs.ma
 212 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
 213 LambdaDelta-1/sn3/defs.ma LambdaDelta-1/pr3/defs.ma
 214 LambdaDelta-1/sn3/fwd.ma LambdaDelta-1/pr3/props.ma LambdaDelta-1/sn3/defs.ma
 215 LambdaDelta-1/sn3/lift1.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/lift1/fwd.ma LambdaDelta-1/sn3/props.ma
 216 LambdaDelta-1/llt/props.ma LambdaDelta-1/leq/defs.ma LambdaDelta-1/llt/defs.ma
 217 LambdaDelta-1/llt/defs.ma LambdaDelta-1/A/defs.ma
 218 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
 219 LambdaDelta-1/ex1/defs.ma LambdaDelta-1/C/defs.ma
 220 LambdaDelta-1/csubst1/props.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/subst1/defs.ma
 221 LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/csubst0/defs.ma
 222 LambdaDelta-1/csubst1/fwd.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/subst1/props.ma
 223 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
 224 Legacy-1/preamble.ma
 225 Legacy-1/spare.ma Legacy-1/theory.ma
 226 Legacy-1/theory.ma Legacy-1/coq/props.ma
 227 Legacy-1/definitions.ma Legacy-1/coq/defs.ma
 228 Legacy-1/coq/props.ma Legacy-1/coq/defs.ma
 229 Legacy-1/coq/defs.ma Legacy-1/preamble.ma
 230 Base-2/preamble.ma Base-1/definitions.ma Legacy-2/theory.ma
 231 Base-1/definitions.ma Base-1/blt/defs.ma Base-1/plist/defs.ma Base-1/types/defs.ma
 232 Base-1/preamble.ma Legacy-1/theory.ma
 233 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
 234 Base-1/spare.ma Base-1/theory.ma
 235 Base-1/plist/props.ma Base-1/plist/defs.ma
 236 Base-1/plist/defs.ma Base-1/preamble.ma
 237 Base-1/ext/tactics.ma Base-1/preamble.ma
 238 Base-1/ext/arith.ma Base-1/preamble.ma
 239 Base-1/types/props.ma Base-1/types/defs.ma
 240 Base-1/types/defs.ma Base-1/preamble.ma
 241 Base-1/blt/props.ma Base-1/blt/defs.ma
 242 Base-1/blt/defs.ma Base-1/preamble.ma
 243 Legacy-2/theory.ma
 244 Legacy-2/coq/defs.mma Legacy-2/preamble.ma Legacy-1/coq/defs.ma
 245 Legacy-2/coq/props.mma Legacy-2/preamble.ma Legacy-1/coq/props.ma
 246 Legacy-2/theory.ma Legacy-2/coq/props.ma