matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/asucc/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/asucc/fwd".
  18
  19 include "asucc/defs.ma".
  20
  21 theorem asucc_gen_sort:
  22  \forall (g: G).(\forall (h: nat).(\forall (n: nat).(\forall (a: A).((eq A
  23 (ASort h n) (asucc g a)) \to (ex_2 nat nat (\lambda (h0: nat).(\lambda (n0:
  24 nat).(eq A a (ASort h0 n0)))))))))
  25 \def
  26  \lambda (g: G).(\lambda (h: nat).(\lambda (n: nat).(\lambda (a: A).(A_ind
  27 (\lambda (a0: A).((eq A (ASort h n) (asucc g a0)) \to (ex_2 nat nat (\lambda
  28 (h0: nat).(\lambda (n0: nat).(eq A a0 (ASort h0 n0))))))) (\lambda (n0:
  29 nat).(\lambda (n1: nat).(\lambda (H: (eq A (ASort h n) (asucc g (ASort n0
  30 n1)))).(let H0 \def (f_equal A A (\lambda (e: A).e) (ASort h n) (match n0
  31 with [O \Rightarrow (ASort O (next g n1)) | (S h) \Rightarrow (ASort h n1)])
  32 H) in (ex_2_intro nat nat (\lambda (h0: nat).(\lambda (n2: nat).(eq A (ASort
  33 n0 n1) (ASort h0 n2)))) n0 n1 (refl_equal A (ASort n0 n1))))))) (\lambda (a0:
  34 A).(\lambda (_: (((eq A (ASort h n) (asucc g a0)) \to (ex_2 nat nat (\lambda
  35 (h0: nat).(\lambda (n0: nat).(eq A a0 (ASort h0 n0)))))))).(\lambda (a1:
  36 A).(\lambda (_: (((eq A (ASort h n) (asucc g a1)) \to (ex_2 nat nat (\lambda
  37 (h0: nat).(\lambda (n0: nat).(eq A a1 (ASort h0 n0)))))))).(\lambda (H1: (eq
  38 A (ASort h n) (asucc g (AHead a0 a1)))).(let H2 \def (eq_ind A (ASort h n)
  39 (\lambda (ee: A).(match ee in A return (\lambda (_: A).Prop) with [(ASort _
  40 _) \Rightarrow True | (AHead _ _) \Rightarrow False])) I (asucc g (AHead a0
  41 a1)) H1) in (False_ind (ex_2 nat nat (\lambda (h0: nat).(\lambda (n0:
  42 nat).(eq A (AHead a0 a1) (ASort h0 n0))))) H2))))))) a)))).
  43
  44 theorem asucc_gen_head:
  45  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (a: A).((eq A
  46 (AHead a1 a2) (asucc g a)) \to (ex2 A (\lambda (a0: A).(eq A a (AHead a1
  47 a0))) (\lambda (a0: A).(eq A a2 (asucc g a0))))))))
  48 \def
  49  \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (a: A).(A_ind
  50 (\lambda (a0: A).((eq A (AHead a1 a2) (asucc g a0)) \to (ex2 A (\lambda (a3:
  51 A).(eq A a0 (AHead a1 a3))) (\lambda (a3: A).(eq A a2 (asucc g a3))))))
  52 (\lambda (n: nat).(\lambda (n0: nat).(\lambda (H: (eq A (AHead a1 a2) (asucc
  53 g (ASort n n0)))).(nat_ind (\lambda (n1: nat).((eq A (AHead a1 a2) (asucc g
  54 (ASort n1 n0))) \to (ex2 A (\lambda (a0: A).(eq A (ASort n1 n0) (AHead a1
  55 a0))) (\lambda (a0: A).(eq A a2 (asucc g a0)))))) (\lambda (H0: (eq A (AHead
  56 a1 a2) (asucc g (ASort O n0)))).(let H1 \def (eq_ind A (AHead a1 a2) (\lambda
  57 (ee: A).(match ee in A return (\lambda (_: A).Prop) with [(ASort _ _)
  58 \Rightarrow False | (AHead _ _) \Rightarrow True])) I (ASort O (next g n0))
  59 H0) in (False_ind (ex2 A (\lambda (a0: A).(eq A (ASort O n0) (AHead a1 a0)))
  60 (\lambda (a0: A).(eq A a2 (asucc g a0)))) H1))) (\lambda (n1: nat).(\lambda
  61 (_: (((eq A (AHead a1 a2) (asucc g (ASort n1 n0))) \to (ex2 A (\lambda (a0:
  62 A).(eq A (ASort n1 n0) (AHead a1 a0))) (\lambda (a0: A).(eq A a2 (asucc g
  63 a0))))))).(\lambda (H0: (eq A (AHead a1 a2) (asucc g (ASort (S n1)
  64 n0)))).(let H1 \def (eq_ind A (AHead a1 a2) (\lambda (ee: A).(match ee in A
  65 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _
  66 _) \Rightarrow True])) I (ASort n1 n0) H0) in (False_ind (ex2 A (\lambda (a0:
  67 A).(eq A (ASort (S n1) n0) (AHead a1 a0))) (\lambda (a0: A).(eq A a2 (asucc g
  68 a0)))) H1))))) n H)))) (\lambda (a0: A).(\lambda (H: (((eq A (AHead a1 a2)
  69 (asucc g a0)) \to (ex2 A (\lambda (a2: A).(eq A a0 (AHead a1 a2))) (\lambda
  70 (a0: A).(eq A a2 (asucc g a0))))))).(\lambda (a3: A).(\lambda (H0: (((eq A
  71 (AHead a1 a2) (asucc g a3)) \to (ex2 A (\lambda (a0: A).(eq A a3 (AHead a1
  72 a0))) (\lambda (a0: A).(eq A a2 (asucc g a0))))))).(\lambda (H1: (eq A (AHead
  73 a1 a2) (asucc g (AHead a0 a3)))).(let H2 \def (f_equal A A (\lambda (e:
  74 A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a1 |
  75 (AHead a _) \Rightarrow a])) (AHead a1 a2) (AHead a0 (asucc g a3)) H1) in
  76 ((let H3 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_:
  77 A).A) with [(ASort _ _) \Rightarrow a2 | (AHead _ a) \Rightarrow a])) (AHead
  78 a1 a2) (AHead a0 (asucc g a3)) H1) in (\lambda (H4: (eq A a1 a0)).(let H5
  79 \def (eq_ind_r A a0 (\lambda (a: A).((eq A (AHead a1 a2) (asucc g a)) \to
  80 (ex2 A (\lambda (a0: A).(eq A a (AHead a1 a0))) (\lambda (a0: A).(eq A a2
  81 (asucc g a0)))))) H a1 H4) in (eq_ind A a1 (\lambda (a4: A).(ex2 A (\lambda
  82 (a5: A).(eq A (AHead a4 a3) (AHead a1 a5))) (\lambda (a5: A).(eq A a2 (asucc
  83 g a5))))) (let H6 \def (eq_ind A a2 (\lambda (a: A).((eq A (AHead a1 a)
  84 (asucc g a3)) \to (ex2 A (\lambda (a0: A).(eq A a3 (AHead a1 a0))) (\lambda
  85 (a0: A).(eq A a (asucc g a0)))))) H0 (asucc g a3) H3) in (let H7 \def (eq_ind
  86 A a2 (\lambda (a: A).((eq A (AHead a1 a) (asucc g a1)) \to (ex2 A (\lambda
  87 (a0: A).(eq A a1 (AHead a1 a0))) (\lambda (a0: A).(eq A a (asucc g a0))))))
  88 H5 (asucc g a3) H3) in (eq_ind_r A (asucc g a3) (\lambda (a4: A).(ex2 A
  89 (\lambda (a5: A).(eq A (AHead a1 a3) (AHead a1 a5))) (\lambda (a5: A).(eq A
  90 a4 (asucc g a5))))) (ex_intro2 A (\lambda (a4: A).(eq A (AHead a1 a3) (AHead
  91 a1 a4))) (\lambda (a4: A).(eq A (asucc g a3) (asucc g a4))) a3 (refl_equal A
  92 (AHead a1 a3)) (refl_equal A (asucc g a3))) a2 H3))) a0 H4)))) H2)))))))
  93 a)))).
  94