helm/software/matita/contribs/ng_assembly/universe/oct.ma

   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 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "universe/universe.ma".
  24
  25 ndefinition OCT_UN ≝ [ uo0; uo1; uo2; uo3; uo4; uo5; uo6; uo7 ].
  26
  27 (* derivati dall'universo
  28   1) SUN_destruct OCT_UN
  29   2) eq_to_eqSUN OCT_UN
  30   3) neq_to_neqSUN OCT_UN
  31   4) eqSUN_to_eq OCT_UN
  32   5) neqSUN_to_neq OCT_UN
  33   6) decidable_SUN OCT_UN
  34   7) symmetric_eqSUN OCT_UN
  35 *)
  36
  37 nlemma un_o0 : S_UN OCT_UN. napply (S_EL OCT_UN uo0 (refl_eq …) ?); #y; nelim y; ##[ ##5: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  38 nlemma un_o1 : S_UN OCT_UN. napply (S_EL OCT_UN uo1 (refl_eq …) ?); #y; nelim y; ##[ ##6: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  39 nlemma un_o2 : S_UN OCT_UN. napply (S_EL OCT_UN uo2 (refl_eq …) ?); #y; nelim y; ##[ ##7: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  40 nlemma un_o3 : S_UN OCT_UN. napply (S_EL OCT_UN uo3 (refl_eq …) ?); #y; nelim y; ##[ ##8: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  41 nlemma un_o4 : S_UN OCT_UN. napply (S_EL OCT_UN uo4 (refl_eq …) ?); #y; nelim y; ##[ ##9: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  42 nlemma un_o5 : S_UN OCT_UN. napply (S_EL OCT_UN uo5 (refl_eq …) ?); #y; nelim y; ##[ ##10: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  43 nlemma un_o6 : S_UN OCT_UN. napply (S_EL OCT_UN uo6 (refl_eq …) ?); #y; nelim y; ##[ ##11: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  44 nlemma un_o7 : S_UN OCT_UN. napply (S_EL OCT_UN uo7 (refl_eq …) ?); #y; nelim y; ##[ ##12: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.