helm/software/matita/contribs/procedural/Coq/Lists/MonoList.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: MonoList.v,v 1.2.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
  34
  35 (*#* THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
  36
  37 include "Arith/Le.ma".
  38
  39 inline procedural "cic:/Coq/Lists/MonoList/List_Dom.con".
  40
  41 inline procedural "cic:/Coq/Lists/MonoList/A.con" as definition.
  42
  43 inline procedural "cic:/Coq/Lists/MonoList/list.ind".
  44
  45 inline procedural "cic:/Coq/Lists/MonoList/app.con" as definition.
  46
  47 inline procedural "cic:/Coq/Lists/MonoList/app_nil_end.con" as lemma.
  48
  49 (* UNEXPORTED
  50 Hint Resolve app_nil_end: list v62.
  51 *)
  52
  53 inline procedural "cic:/Coq/Lists/MonoList/app_ass.con" as lemma.
  54
  55 (* UNEXPORTED
  56 Hint Resolve app_ass: list v62.
  57 *)
  58
  59 inline procedural "cic:/Coq/Lists/MonoList/ass_app.con" as lemma.
  60
  61 (* UNEXPORTED
  62 Hint Resolve ass_app: list v62.
  63 *)
  64
  65 inline procedural "cic:/Coq/Lists/MonoList/tail.con" as definition.
  66
  67 inline procedural "cic:/Coq/Lists/MonoList/nil_cons.con" as lemma.
  68
  69 (*#***************************************)
  70
  71 (* Length of lists                      *)
  72
  73 (*#***************************************)
  74
  75 inline procedural "cic:/Coq/Lists/MonoList/length.con" as definition.
  76
  77 (*#*****************************)
  78
  79 (* Length order of lists      *)
  80
  81 (*#*****************************)
  82
  83 (* UNEXPORTED
  84 Section length_order
  85 *)
  86
  87 inline procedural "cic:/Coq/Lists/MonoList/lel.con" as definition.
  88
  89 (* UNEXPORTED
  90 Hint Unfold lel: list.
  91 *)
  92
  93 (* UNEXPORTED
  94 cic:/Coq/Lists/MonoList/length_order/a.var
  95 *)
  96
  97 (* UNEXPORTED
  98 cic:/Coq/Lists/MonoList/length_order/b.var
  99 *)
 100
 101 (* UNEXPORTED
 102 cic:/Coq/Lists/MonoList/length_order/l.var
 103 *)
 104
 105 (* UNEXPORTED
 106 cic:/Coq/Lists/MonoList/length_order/m.var
 107 *)
 108
 109 (* UNEXPORTED
 110 cic:/Coq/Lists/MonoList/length_order/n.var
 111 *)
 112
 113 inline procedural "cic:/Coq/Lists/MonoList/lel_refl.con" as lemma.
 114
 115 inline procedural "cic:/Coq/Lists/MonoList/lel_trans.con" as lemma.
 116
 117 inline procedural "cic:/Coq/Lists/MonoList/lel_cons_cons.con" as lemma.
 118
 119 inline procedural "cic:/Coq/Lists/MonoList/lel_cons.con" as lemma.
 120
 121 inline procedural "cic:/Coq/Lists/MonoList/lel_tail.con" as lemma.
 122
 123 inline procedural "cic:/Coq/Lists/MonoList/lel_nil.con" as lemma.
 124
 125 (* UNEXPORTED
 126 End length_order
 127 *)
 128
 129 (* UNEXPORTED
 130 Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
 131   v62.
 132 *)
 133
 134 inline procedural "cic:/Coq/Lists/MonoList/In.con" as definition.
 135
 136 inline procedural "cic:/Coq/Lists/MonoList/in_eq.con" as lemma.
 137
 138 (* UNEXPORTED
 139 Hint Resolve in_eq: list v62.
 140 *)
 141
 142 inline procedural "cic:/Coq/Lists/MonoList/in_cons.con" as lemma.
 143
 144 (* UNEXPORTED
 145 Hint Resolve in_cons: list v62.
 146 *)
 147
 148 inline procedural "cic:/Coq/Lists/MonoList/in_app_or.con" as lemma.
 149
 150 (* UNEXPORTED
 151 Hint Immediate in_app_or: list v62.
 152 *)
 153
 154 inline procedural "cic:/Coq/Lists/MonoList/in_or_app.con" as lemma.
 155
 156 (* UNEXPORTED
 157 Hint Resolve in_or_app: list v62.
 158 *)
 159
 160 inline procedural "cic:/Coq/Lists/MonoList/incl.con" as definition.
 161
 162 (* UNEXPORTED
 163 Hint Unfold incl: list v62.
 164 *)
 165
 166 inline procedural "cic:/Coq/Lists/MonoList/incl_refl.con" as lemma.
 167
 168 (* UNEXPORTED
 169 Hint Resolve incl_refl: list v62.
 170 *)
 171
 172 inline procedural "cic:/Coq/Lists/MonoList/incl_tl.con" as lemma.
 173
 174 (* UNEXPORTED
 175 Hint Immediate incl_tl: list v62.
 176 *)
 177
 178 inline procedural "cic:/Coq/Lists/MonoList/incl_tran.con" as lemma.
 179
 180 inline procedural "cic:/Coq/Lists/MonoList/incl_appl.con" as lemma.
 181
 182 (* UNEXPORTED
 183 Hint Immediate incl_appl: list v62.
 184 *)
 185
 186 inline procedural "cic:/Coq/Lists/MonoList/incl_appr.con" as lemma.
 187
 188 (* UNEXPORTED
 189 Hint Immediate incl_appr: list v62.
 190 *)
 191
 192 inline procedural "cic:/Coq/Lists/MonoList/incl_cons.con" as lemma.
 193
 194 (* UNEXPORTED
 195 Hint Resolve incl_cons: list v62.
 196 *)
 197
 198 inline procedural "cic:/Coq/Lists/MonoList/incl_app.con" as lemma.
 199
 200 (* UNEXPORTED
 201 Hint Resolve incl_app: list v62.
 202 *)
 203