helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd.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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd".
  18
  19 include "subst0/defs.ma".
  20
  21 include "lift/props.ma".
  22
  23 axiom subst0_gen_sort:
  24  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst0
  25 i v (TSort n) x) \to (\forall (P: Prop).P)))))
  26 .
  27
  28 axiom subst0_gen_lref:
  29  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst0
  30 i v (TLRef n) x) \to (land (eq nat n i) (eq T x (lift (S n) O v)))))))
  31 .
  32
  33 axiom subst0_gen_head:
  34  \forall (k: K).(\forall (v: T).(\forall (u1: T).(\forall (t1: T).(\forall
  35 (x: T).(\forall (i: nat).((subst0 i v (THead k u1 t1) x) \to (or3 (ex2 T
  36 (\lambda (u2: T).(eq T x (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1
  37 u2))) (ex2 T (\lambda (t2: T).(eq T x (THead k u1 t2))) (\lambda (t2:
  38 T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
  39 T).(eq T x (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v u1
  40 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))))))))
  41 .
  42
  43 axiom subst0_gen_lift_lt:
  44  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall
  45 (h: nat).(\forall (d: nat).((subst0 i (lift h d u) (lift h (S (plus i d)) t1)
  46 x) \to (ex2 T (\lambda (t2: T).(eq T x (lift h (S (plus i d)) t2))) (\lambda
  47 (t2: T).(subst0 i u t1 t2)))))))))
  48 .
  49
  50 axiom subst0_gen_lift_false:
  51  \forall (t: T).(\forall (u: T).(\forall (x: T).(\forall (h: nat).(\forall
  52 (d: nat).(\forall (i: nat).((le d i) \to ((lt i (plus d h)) \to ((subst0 i u
  53 (lift h d t) x) \to (\forall (P: Prop).P)))))))))
  54 .
  55
  56 axiom subst0_gen_lift_ge:
  57  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall
  58 (h: nat).(\forall (d: nat).((subst0 i u (lift h d t1) x) \to ((le (plus d h)
  59 i) \to (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2:
  60 T).(subst0 (minus i h) u t1 t2))))))))))
  61 .
  62