matita/matita/contribs/lambdadelta/basic_1A/spare.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 (* This file was automatically generated: do not edit *********************)
  16
  17 include "basic_1A/theory.ma".
  18
  19 axiom pc3_gen_appls_sort_abst:
  20  \forall (c: C).(\forall (vs: TList).(\forall (w: T).(\forall (u: T).(\forall
  21 (n: nat).((pc3 c (THeads (Flat Appl) vs (TSort n)) (THead (Bind Abst) w u))
  22 \to False)))))
  23 .
  24
  25 axiom pc3_gen_appls_lref_abst:
  26  \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
  27 (CHead d (Bind Abst) v)) \to (\forall (vs: TList).(\forall (w: T).(\forall
  28 (u: T).((pc3 c (THeads (Flat Appl) vs (TLRef i)) (THead (Bind Abst) w u)) \to
  29 False))))))))
  30 .
  31
  32 axiom pc3_gen_appls_lref_sort:
  33  \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
  34 (CHead d (Bind Abst) v)) \to (\forall (vs: TList).(\forall (ws:
  35 TList).(\forall (n: nat).((pc3 c (THeads (Flat Appl) vs (TLRef i)) (THeads
  36 (Flat Appl) ws (TSort n))) \to False))))))))
  37 .
  38