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

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