helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.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 (*s Instantiating [eqN] with Leibniz equality *)
  20
  21 include "Num/NSyntax.ma".
  22
  23 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eqN.con" as definition.
  24
  25 (* UNEXPORTED
  26 Hints Unfold eqN : num.
  27 *)
  28
  29 (* NOTATION
  30 Grammar constr constr1 :=
  31 eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
  32 *)
  33
  34 (* NOTATION
  35 Syntax constr
  36   level 1:
  37     equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ].
  38 *)
  39
  40 (*s Lemmas for [eqN] *)
  41
  42 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_refl.con" as lemma.
  43
  44 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_sym.con" as lemma.
  45
  46 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_trans.con" as lemma.
  47
  48 (* UNEXPORTED
  49 Hints Resolve eq_refl eq_trans : num.
  50 *)
  51
  52 (* UNEXPORTED
  53 Hints Immediate eq_sym : num.
  54 *)
  55
  56 (*s Compatibility lemmas for [S], [add], [lt] *)
  57
  58 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/S_eq_compat.con" as lemma.
  59
  60 (* UNEXPORTED
  61 Hints Resolve S_eq_compat : nat.
  62 *)
  63
  64 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/add_eq_compat.con" as lemma.
  65
  66 (* UNEXPORTED
  67 Hints Resolve add_eq_compat : nat.
  68 *)
  69
  70 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/lt_eq_compat.con" as lemma.
  71
  72 (* UNEXPORTED
  73 Hints Resolve add_eq_compat S_eq_compat lt_eq_compat : num.
  74 *)
  75