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

   1 theory.ma ex0/props.ma ex1/props.ma ex2/props.ma pr3/wcpr0.ma subst0/tlt.ma tau1/cnt.ma ty3/dec.ma ty3/nf2.ma ty3/tau0.ma wcpr0/fwd.ma
   2 spare.ma theory.ma
   3 preamble.ma ../Base-1/theory.ma
   4 definitions.ma aprem/defs.ma cimp/defs.ma clen/defs.ma cnt/defs.ma csuba/defs.ma csubc/defs.ma csubst1/defs.ma csubt/defs.ma ex0/defs.ma ex1/defs.ma ex2/defs.ma flt/defs.ma fsubst0/defs.ma iso/defs.ma llt/defs.ma next_plus/defs.ma nf2/defs.ma pc1/defs.ma subst1/defs.ma tau1/defs.ma tlt/defs.ma wcpr0/defs.ma
   5 ex0/defs.ma A/defs.ma G/defs.ma
   6 ex0/props.ma aplus/props.ma ex0/defs.ma leq/defs.ma
   7 ex2/defs.ma C/defs.ma
   8 ex2/props.ma arity/fwd.ma ex2/defs.ma nf2/defs.ma pr2/fwd.ma
   9 tlist/defs.ma T/defs.ma
  10 tlist/props.ma tlist/defs.ma
  11 csubt/defs.ma ty3/defs.ma
  12 csubt/fwd.ma csubt/defs.ma
  13 csubt/props.ma csubt/defs.ma
  14 csubt/clear.ma clear/fwd.ma csubt/defs.ma
  15 csubt/drop.ma csubt/defs.ma drop/fwd.ma
  16 csubt/getl.ma csubt/clear.ma csubt/drop.ma csubt/fwd.ma getl/clear.ma
  17 csubt/pc3.ma csubt/getl.ma pc3/left.ma
  18 csubt/ty3.ma csubt/pc3.ma csubt/props.ma
  19 csubc/defs.ma sc3/defs.ma
  20 csubc/props.ma csubc/defs.ma sc3/props.ma
  21 csubc/csuba.ma csuba/defs.ma csubc/defs.ma sc3/props.ma
  22 csubc/drop.ma csubc/defs.ma sc3/props.ma
  23 csubc/drop1.ma csubc/drop.ma
  24 csubc/clear.ma csubc/defs.ma
  25 csubc/getl.ma csubc/clear.ma csubc/drop.ma
  26 csubc/arity.ma arity/defs.ma csubc/csuba.ma
  27 ty3/fsubst0.ma csubst0/props.ma getl/getl.ma pc3/fsubst0.ma ty3/props.ma
  28 ty3/defs.ma G/defs.ma pc3/defs.ma
  29 ty3/fwd.ma pc3/props.ma ty3/defs.ma
  30 ty3/props.ma pc3/fwd.ma ty3/fwd.ma
  31 ty3/subst1.ma csubst1/fwd.ma csubst1/getl.ma getl/getl.ma pc3/fwd.ma pc3/subst1.ma ty3/props.ma
  32 ty3/pr3_props.ma ty3/pr3.ma
  33 ty3/pr3.ma csubt/ty3.ma pc1/props.ma pc3/pc1.ma pc3/wcpr0.ma ty3/fsubst0.ma ty3/subst1.ma
  34 ty3/tau0.ma tau0/defs.ma ty3/pr3_props.ma
  35 ty3/arity.ma arity/pr3.ma asucc/fwd.ma ty3/pr3_props.ma
  36 ty3/dec.ma getl/dec.ma getl/flt.ma pc3/dec.ma ty3/pr3_props.ma
  37 ty3/arity_props.ma sc3/arity.ma ty3/arity.ma ty3/fwd.ma
  38 ty3/nf2.ma nf2/arity.ma pc3/nf2.ma ty3/arity.ma
  39 pc3/defs.ma pr3/defs.ma
  40 pc3/props.ma pc3/defs.ma pr3/pr3.ma
  41 pc3/fsubst0.ma csubst0/getl.ma fsubst0/defs.ma pc3/left.ma
  42 pc3/pc1.ma pc1/defs.ma pc3/defs.ma pr3/pr1.ma
  43 pc3/wcpr0.ma pc3/props.ma wcpr0/getl.ma
  44 pc3/left.ma pc3/props.ma
  45 pc3/fwd.ma pc3/props.ma pr3/fwd.ma
  46 pc3/nf2.ma nf2/pr3.ma pc3/defs.ma
  47 pc3/subst1.ma pc3/props.ma pr3/subst1.ma
  48 pc3/dec.ma nf2/fwd.ma ty3/arity_props.ma ty3/pr3.ma
  49 pc1/defs.ma pr1/defs.ma
  50 pc1/props.ma pc1/defs.ma pr1/pr1.ma
  51 ex1/defs.ma C/defs.ma
  52 ex1/props.ma arity/defs.ma ex1/defs.ma leq/props.ma nf2/pr3.ma nf2/props.ma pc3/fwd.ma ty3/fwd.ma
  53 sc3/defs.ma arity/defs.ma drop1/defs.ma sn3/defs.ma
  54 sc3/props.ma arity/aprem.ma arity/lift1.ma csuba/arity.ma drop1/getl.ma drop1/props.ma lift1/props.ma llt/props.ma nf2/lift1.ma sc3/defs.ma sn3/lift1.ma
  55 sc3/arity.ma csubc/arity.ma csubc/drop1.ma csubc/getl.ma csubc/props.ma
  56 sn3/defs.ma pr3/defs.ma
  57 sn3/nf2.ma nf2/dec.ma nf2/pr3.ma sn3/defs.ma
  58 sn3/props.ma iso/props.ma nf2/iso.ma pr3/iso.ma sn3/fwd.ma sn3/nf2.ma
  59 sn3/lift1.ma drop1/defs.ma lift1/fwd.ma sn3/props.ma
  60 sn3/fwd.ma pr3/props.ma sn3/defs.ma
  61 nf2/defs.ma pr2/defs.ma
  62 nf2/fwd.ma T/props.ma nf2/defs.ma pr2/clen.ma subst0/dec.ma
  63 nf2/props.ma nf2/defs.ma pr2/fwd.ma
  64 nf2/arity.ma arity/subst0.ma nf2/fwd.ma
  65 nf2/pr3.ma nf2/defs.ma pr3/pr3.ma
  66 nf2/lift1.ma drop1/defs.ma nf2/props.ma
  67 nf2/iso.ma iso/props.ma nf2/pr3.ma pr3/fwd.ma
  68 nf2/dec.ma C/props.ma nf2/defs.ma pr0/dec.ma pr2/clen.ma pr2/fwd.ma
  69 csuba/defs.ma arity/defs.ma
  70 csuba/fwd.ma csuba/defs.ma
  71 csuba/props.ma csuba/defs.ma
  72 csuba/arity.ma T/props.ma arity/props.ma csuba/getl.ma csuba/props.ma
  73 csuba/clear.ma clear/fwd.ma csuba/defs.ma
  74 csuba/drop.ma csuba/fwd.ma drop/fwd.ma
  75 csuba/getl.ma csuba/clear.ma csuba/drop.ma getl/clear.ma
  76 wcpr0/getl.ma getl/props.ma wcpr0/defs.ma
  77 wcpr0/fwd.ma wcpr0/defs.ma
  78 wcpr0/defs.ma C/defs.ma pr0/defs.ma
  79 pr3/defs.ma pr2/defs.ma
  80 pr3/subst1.ma pr2/subst1.ma pr3/defs.ma
  81 pr3/props.ma pr1/props.ma pr2/props.ma pr3/pr1.ma
  82 pr3/pr1.ma pr1/defs.ma pr3/defs.ma
  83 pr3/wcpr0.ma pr3/props.ma wcpr0/getl.ma
  84 pr3/fwd.ma pr2/fwd.ma pr3/props.ma
  85 pr3/pr3.ma pr2/pr2.ma pr3/props.ma
  86 pr3/iso.ma iso/props.ma pr3/fwd.ma tlist/props.ma
  87 pr2/defs.ma getl/defs.ma pr0/defs.ma
  88 pr2/props.ma getl/clear.ma getl/drop.ma pr0/props.ma pr2/defs.ma
  89 pr2/fwd.ma getl/clear.ma getl/drop.ma pr0/fwd.ma pr2/defs.ma
  90 pr2/subst1.ma csubst1/fwd.ma csubst1/getl.ma getl/drop.ma pr0/fwd.ma pr0/subst1.ma pr2/defs.ma subst1/subst1.ma
  91 pr2/clen.ma clen/getl.ma pr2/props.ma
  92 pr2/pr2.ma getl/props.ma pr0/pr0.ma pr2/defs.ma
  93 pr1/defs.ma pr0/defs.ma
  94 pr1/props.ma T/props.ma pr0/subst1.ma pr1/defs.ma subst1/props.ma
  95 pr1/pr1.ma pr0/pr0.ma pr1/props.ma
  96 pr0/subst1.ma pr0/props.ma subst1/defs.ma
  97 pr0/defs.ma subst0/defs.ma
  98 pr0/fwd.ma pr0/props.ma
  99 pr0/props.ma pr0/defs.ma subst0/subst0.ma
 100 pr0/pr0.ma lift/tlt.ma pr0/fwd.ma
 101 pr0/dec.ma T/dec.ma T/props.ma pr0/fwd.ma subst0/dec.ma
 102 tau1/defs.ma tau0/defs.ma
 103 tau1/props.ma tau0/props.ma tau1/defs.ma
 104 tau1/cnt.ma cnt/props.ma tau1/props.ma
 105 arity/defs.ma getl/defs.ma leq/defs.ma
 106 arity/fwd.ma arity/defs.ma getl/drop.ma leq/asucc.ma leq/fwd.ma
 107 arity/subst0.ma arity/props.ma csubst0/getl.ma csubst0/props.ma fsubst0/fwd.ma getl/getl.ma subst0/dec.ma subst0/fwd.ma
 108 arity/props.ma arity/fwd.ma
 109 arity/pr3.ma arity/subst0.ma csuba/arity.ma pr0/fwd.ma pr1/defs.ma pr3/defs.ma wcpr0/getl.ma
 110 arity/lift1.ma arity/props.ma drop1/defs.ma
 111 arity/cimp.ma arity/defs.ma cimp/props.ma
 112 arity/aprem.ma aprem/props.ma arity/cimp.ma arity/props.ma
 113 aprem/defs.ma A/defs.ma
 114 aprem/props.ma aprem/defs.ma leq/defs.ma
 115 llt/defs.ma A/defs.ma
 116 llt/props.ma leq/defs.ma llt/defs.ma
 117 leq/defs.ma aplus/defs.ma
 118 leq/asucc.ma aplus/props.ma leq/props.ma
 119 leq/props.ma aplus/props.ma leq/defs.ma
 120 leq/fwd.ma leq/defs.ma
 121 aplus/defs.ma asucc/defs.ma
 122 aplus/props.ma aplus/defs.ma next_plus/props.ma
 123 asucc/defs.ma A/defs.ma G/defs.ma
 124 asucc/fwd.ma asucc/defs.ma
 125 A/defs.ma preamble.ma
 126 fsubst0/defs.ma csubst0/defs.ma subst0/defs.ma
 127 fsubst0/fwd.ma fsubst0/defs.ma
 128 csubst1/defs.ma csubst0/defs.ma
 129 csubst1/props.ma csubst1/defs.ma subst1/defs.ma
 130 csubst1/fwd.ma csubst0/fwd.ma csubst1/defs.ma subst1/props.ma
 131 csubst1/getl.ma csubst0/getl.ma csubst0/props.ma csubst1/props.ma drop/props.ma subst1/props.ma
 132 csubst0/defs.ma C/defs.ma subst0/defs.ma
 133 csubst0/fwd.ma csubst0/defs.ma
 134 csubst0/props.ma csubst0/defs.ma
 135 csubst0/drop.ma csubst0/fwd.ma drop/fwd.ma s/props.ma
 136 csubst0/clear.ma clear/fwd.ma csubst0/fwd.ma
 137 csubst0/getl.ma csubst0/clear.ma csubst0/drop.ma getl/fwd.ma
 138 subst0/defs.ma lift/defs.ma
 139 subst0/fwd.ma lift/props.ma subst0/defs.ma
 140 subst0/subst0.ma subst0/props.ma
 141 subst0/props.ma lift/props.ma subst0/fwd.ma
 142 subst0/tlt.ma lift/props.ma lift/tlt.ma subst0/defs.ma
 143 subst0/dec.ma lift/props.ma subst0/defs.ma
 144 tau0/defs.ma G/defs.ma getl/defs.ma
 145 tau0/props.ma getl/drop.ma tau0/defs.ma
 146 subst1/subst1.ma subst0/subst0.ma subst1/fwd.ma
 147 subst1/defs.ma subst0/defs.ma
 148 subst1/fwd.ma subst0/props.ma subst1/defs.ma
 149 subst1/props.ma subst0/props.ma subst1/defs.ma
 150 cimp/defs.ma getl/defs.ma
 151 cimp/props.ma cimp/defs.ma getl/getl.ma
 152 getl/defs.ma clear/defs.ma drop/defs.ma
 153 getl/props.ma clear/props.ma drop/props.ma getl/fwd.ma
 154 getl/fwd.ma clear/fwd.ma drop/fwd.ma getl/defs.ma
 155 getl/drop.ma clear/drop.ma getl/props.ma r/props.ma
 156 getl/clear.ma clear/drop.ma getl/props.ma
 157 getl/getl.ma getl/clear.ma getl/drop.ma
 158 getl/dec.ma getl/props.ma
 159 getl/flt.ma clear/props.ma flt/props.ma getl/fwd.ma
 160 clear/defs.ma C/defs.ma
 161 clear/fwd.ma clear/defs.ma
 162 clear/props.ma clear/fwd.ma
 163 clear/drop.ma clear/fwd.ma drop/fwd.ma
 164 drop1/defs.ma drop/defs.ma lift1/defs.ma
 165 drop1/props.ma drop/props.ma drop1/defs.ma getl/defs.ma
 166 drop1/getl.ma drop1/defs.ma getl/drop.ma
 167 drop/defs.ma C/defs.ma lift/defs.ma r/defs.ma
 168 drop/fwd.ma drop/defs.ma
 169 drop/props.ma drop/fwd.ma lift/props.ma r/props.ma
 170 lift1/defs.ma lift/defs.ma
 171 lift1/fwd.ma lift/fwd.ma lift1/defs.ma
 172 lift1/props.ma drop1/defs.ma lift/props.ma lift1/defs.ma
 173 cnt/defs.ma T/defs.ma
 174 cnt/props.ma cnt/defs.ma lift/fwd.ma
 175 lift/defs.ma T/defs.ma s/defs.ma tlist/defs.ma
 176 lift/fwd.ma lift/defs.ma
 177 lift/props.ma lift/fwd.ma s/props.ma tlist/defs.ma
 178 lift/tlt.ma lift/fwd.ma tlt/props.ma
 179 iso/props.ma iso/fwd.ma
 180 iso/fwd.ma iso/defs.ma tlist/defs.ma
 181 iso/defs.ma T/defs.ma
 182 G/defs.ma preamble.ma
 183 flt/props.ma C/props.ma flt/defs.ma
 184 flt/defs.ma C/defs.ma
 185 tlt/props.ma tlt/defs.ma
 186 tlt/defs.ma T/defs.ma
 187 T/props.ma T/defs.ma
 188 T/dec.ma T/defs.ma
 189 T/defs.ma preamble.ma
 190 s/props.ma s/defs.ma
 191 s/defs.ma T/defs.ma
 192 C/props.ma C/defs.ma T/props.ma
 193 C/defs.ma T/defs.ma
 194 r/props.ma r/defs.ma s/defs.ma
 195 r/defs.ma T/defs.ma
 196 next_plus/props.ma next_plus/defs.ma
 197 next_plus/defs.ma G/defs.ma
 198 clen/getl.ma clen/defs.ma getl/props.ma
 199 clen/defs.ma C/defs.ma s/defs.ma
 200 ../Base-1/theory.ma