matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/aprem.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/arity/aprem".
  18
  19 include "arity/props.ma".
  20
  21 include "arity/cimp.ma".
  22
  23 include "aprem/props.ma".
  24
  25 theorem arity_aprem:
  26  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
  27 a) \to (\forall (i: nat).(\forall (b: A).((aprem i a b) \to (ex2_3 C T nat
  28 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c))))
  29 (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc g
  30 b)))))))))))))
  31 \def
  32  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H:
  33 (arity g c t a)).(arity_ind g (\lambda (c0: C).(\lambda (_: T).(\lambda (a0:
  34 A).(\forall (i: nat).(\forall (b: A).((aprem i a0 b) \to (ex2_3 C T nat
  35 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0))))
  36 (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc g
  37 b)))))))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (i: nat).(\lambda
  38 (b: A).(\lambda (H0: (aprem i (ASort O n) b)).(let H1 \def (match H0 in aprem
  39 return (\lambda (n0: nat).(\lambda (a0: A).(\lambda (a1: A).(\lambda (_:
  40 (aprem n0 a0 a1)).((eq nat n0 i) \to ((eq A a0 (ASort O n)) \to ((eq A a1 b)
  41 \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
  42 (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_:
  43 nat).(arity g d u (asucc g b))))))))))))) with [(aprem_zero a1 a2)
  44 \Rightarrow (\lambda (H1: (eq nat O i)).(\lambda (H2: (eq A (AHead a1 a2)
  45 (ASort O n))).(\lambda (H3: (eq A a1 b)).(eq_ind nat O (\lambda (n0:
  46 nat).((eq A (AHead a1 a2) (ASort O n)) \to ((eq A a1 b) \to (ex2_3 C T nat
  47 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus n0 j) O d
  48 c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc
  49 g b))))))))) (\lambda (H4: (eq A (AHead a1 a2) (ASort O n))).(let H5 \def
  50 (eq_ind A (AHead a1 a2) (\lambda (e: A).(match e in A return (\lambda (_:
  51 A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow
  52 True])) I (ASort O n) H4) in (False_ind ((eq A a1 b) \to (ex2_3 C T nat
  53 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0))))
  54 (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc g
  55 b))))))) H5))) i H1 H2 H3)))) | (aprem_succ a2 a0 i0 H1 a1) \Rightarrow
  56 (\lambda (H2: (eq nat (S i0) i)).(\lambda (H3: (eq A (AHead a1 a2) (ASort O
  57 n))).(\lambda (H4: (eq A a0 b)).(eq_ind nat (S i0) (\lambda (n0: nat).((eq A
  58 (AHead a1 a2) (ASort O n)) \to ((eq A a0 b) \to ((aprem i0 a2 a0) \to (ex2_3
  59 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus n0 j) O
  60 d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u
  61 (asucc g b)))))))))) (\lambda (H5: (eq A (AHead a1 a2) (ASort O n))).(let H6
  62 \def (eq_ind A (AHead a1 a2) (\lambda (e: A).(match e in A return (\lambda
  63 (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow
  64 True])) I (ASort O n) H5) in (False_ind ((eq A a0 b) \to ((aprem i0 a2 a0)
  65 \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
  66 (plus (S i0) j) O d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_:
  67 nat).(arity g d u (asucc g b)))))))) H6))) i H2 H3 H4 H1))))]) in (H1
  68 (refl_equal nat i) (refl_equal A (ASort O n)) (refl_equal A b))))))))
  69 (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
  70 (H0: (getl i c0 (CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (_:
  71 (arity g d u a0)).(\lambda (H2: ((\forall (i0: nat).(\forall (b: A).((aprem
  72 i0 a0 b) \to (ex2_3 C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
  73 nat).(drop (plus i0 j) O d0 d)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda
  74 (_: nat).(arity g d0 u0 (asucc g b))))))))))).(\lambda (i0: nat).(\lambda (b:
  75 A).(\lambda (H3: (aprem i0 a0 b)).(let H_x \def (H2 i0 b H3) in (let H4 \def
  76 H_x in (ex2_3_ind C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
  77 nat).(drop (plus i0 j) O d0 d)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda
  78 (_: nat).(arity g d0 u0 (asucc g b))))) (ex2_3 C T nat (\lambda (d0:
  79 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i0 j) O d0 c0)))) (\lambda
  80 (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))))
  81 (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: nat).(\lambda (H5: (drop
  82 (plus i0 x2) O x0 d)).(\lambda (H6: (arity g x0 x1 (asucc g b))).(let H_x0
  83 \def (getl_drop_conf_rev (plus i0 x2) x0 d H5 Abbr c0 u i H0) in (let H7 \def
  84 H_x0 in (ex2_ind C (\lambda (c1: C).(drop (plus i0 x2) O c1 c0)) (\lambda
  85 (c1: C).(drop (S i) (plus i0 x2) c1 x0)) (ex2_3 C T nat (\lambda (d0:
  86 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i0 j) O d0 c0)))) (\lambda
  87 (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))))
  88 (\lambda (x: C).(\lambda (H8: (drop (plus i0 x2) O x c0)).(\lambda (H9: (drop
  89 (S i) (plus i0 x2) x x0)).(ex2_3_intro C T nat (\lambda (d0: C).(\lambda (_:
  90 T).(\lambda (j: nat).(drop (plus i0 j) O d0 c0)))) (\lambda (d0: C).(\lambda
  91 (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))) x (lift (S i) (plus
  92 i0 x2) x1) x2 H8 (arity_lift g x0 x1 (asucc g b) H6 x (S i) (plus i0 x2)
  93 H9))))) H7)))))))) H4)))))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda
  94 (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abst)
  95 u))).(\lambda (a0: A).(\lambda (_: (arity g d u (asucc g a0))).(\lambda (H2:
  96 ((\forall (i0: nat).(\forall (b: A).((aprem i0 (asucc g a0) b) \to (ex2_3 C T
  97 nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i0 j) O d0
  98 d)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
  99 (asucc g b))))))))))).(\lambda (i0: nat).(\lambda (b: A).(\lambda (H3: (aprem
 100 i0 a0 b)).(let H4 \def (H2 i0 b (aprem_asucc g a0 b i0 H3)) in (ex2_3_ind C T
 101 nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i0 j) O d0
 102 d)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
 103 (asucc g b))))) (ex2_3 C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
 104 nat).(drop (plus i0 j) O d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda
 105 (_: nat).(arity g d0 u0 (asucc g b)))))) (\lambda (x0: C).(\lambda (x1:
 106 T).(\lambda (x2: nat).(\lambda (H5: (drop (plus i0 x2) O x0 d)).(\lambda (H6:
 107 (arity g x0 x1 (asucc g b))).(let H_x \def (getl_drop_conf_rev (plus i0 x2)
 108 x0 d H5 Abst c0 u i H0) in (let H7 \def H_x in (ex2_ind C (\lambda (c1:
 109 C).(drop (plus i0 x2) O c1 c0)) (\lambda (c1: C).(drop (S i) (plus i0 x2) c1
 110 x0)) (ex2_3 C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop
 111 (plus i0 j) O d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_:
 112 nat).(arity g d0 u0 (asucc g b)))))) (\lambda (x: C).(\lambda (H8: (drop
 113 (plus i0 x2) O x c0)).(\lambda (H9: (drop (S i) (plus i0 x2) x
 114 x0)).(ex2_3_intro C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
 115 nat).(drop (plus i0 j) O d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda
 116 (_: nat).(arity g d0 u0 (asucc g b))))) x (lift (S i) (plus i0 x2) x1) x2 H8
 117 (arity_lift g x0 x1 (asucc g b) H6 x (S i) (plus i0 x2) H9))))) H7))))))))
 118 H4))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda
 119 (c0: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u
 120 a1)).(\lambda (_: ((\forall (i: nat).(\forall (b0: A).((aprem i a1 b0) \to
 121 (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus
 122 i j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d
 123 u0 (asucc g b0))))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_:
 124 (arity g (CHead c0 (Bind b) u) t0 a2)).(\lambda (H4: ((\forall (i:
 125 nat).(\forall (b0: A).((aprem i a2 b0) \to (ex2_3 C T nat (\lambda (d:
 126 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d (CHead c0 (Bind b)
 127 u))))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
 128 (asucc g b0))))))))))).(\lambda (i: nat).(\lambda (b0: A).(\lambda (H5:
 129 (aprem i a2 b0)).(let H_x \def (H4 i b0 H5) in (let H6 \def H_x in (ex2_3_ind
 130 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O
 131 d (CHead c0 (Bind b) u))))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
 132 nat).(arity g d u0 (asucc g b0))))) (ex2_3 C T nat (\lambda (d: C).(\lambda
 133 (_: T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda
 134 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b0)))))) (\lambda (x0:
 135 C).(\lambda (x1: T).(\lambda (x2: nat).(\lambda (H7: (drop (plus i x2) O x0
 136 (CHead c0 (Bind b) u))).(\lambda (H8: (arity g x0 x1 (asucc g b0))).(let H9
 137 \def (eq_ind nat (S (plus i x2)) (\lambda (n: nat).(drop n O x0 c0)) (drop_S
 138 b x0 c0 u (plus i x2) H7) (plus i (S x2)) (plus_n_Sm i x2)) in (ex2_3_intro C
 139 T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d
 140 c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
 141 (asucc g b0))))) x0 x1 (S x2) H9 H8))))))) H6))))))))))))))))) (\lambda (c0:
 142 C).(\lambda (u: T).(\lambda (a1: A).(\lambda (H0: (arity g c0 u (asucc g
 143 a1))).(\lambda (_: ((\forall (i: nat).(\forall (b: A).((aprem i (asucc g a1)
 144 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
 145 (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
 146 nat).(arity g d u0 (asucc g b))))))))))).(\lambda (t0: T).(\lambda (a2:
 147 A).(\lambda (_: (arity g (CHead c0 (Bind Abst) u) t0 a2)).(\lambda (H3:
 148 ((\forall (i: nat).(\forall (b: A).((aprem i a2 b) \to (ex2_3 C T nat
 149 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d (CHead
 150 c0 (Bind Abst) u))))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
 151 nat).(arity g d u0 (asucc g b))))))))))).(\lambda (i: nat).(\lambda (b:
 152 A).(\lambda (H4: (aprem i (AHead a1 a2) b)).((match i in nat return (\lambda
 153 (n: nat).((aprem n (AHead a1 a2) b) \to (ex2_3 C T nat (\lambda (d:
 154 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus n j) O d c0)))) (\lambda (d:
 155 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))))) with
 156 [O \Rightarrow (\lambda (H5: (aprem O (AHead a1 a2) b)).(let H6 \def (match
 157 H5 in aprem return (\lambda (n: nat).(\lambda (a0: A).(\lambda (a3:
 158 A).(\lambda (_: (aprem n a0 a3)).((eq nat n O) \to ((eq A a0 (AHead a1 a2))
 159 \to ((eq A a3 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda
 160 (j: nat).(drop (plus O j) O d c0)))) (\lambda (d: C).(\lambda (u0:
 161 T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))))))) with [(aprem_zero
 162 a0 a3) \Rightarrow (\lambda (_: (eq nat O O)).(\lambda (H7: (eq A (AHead a0
 163 a3) (AHead a1 a2))).(\lambda (H8: (eq A a0 b)).((let H9 \def (f_equal A A
 164 (\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _)
 165 \Rightarrow a3 | (AHead _ a4) \Rightarrow a4])) (AHead a0 a3) (AHead a1 a2)
 166 H7) in ((let H10 \def (f_equal A A (\lambda (e: A).(match e in A return
 167 (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a0 | (AHead a4 _)
 168 \Rightarrow a4])) (AHead a0 a3) (AHead a1 a2) H7) in (eq_ind A a1 (\lambda
 169 (a4: A).((eq A a3 a2) \to ((eq A a4 b) \to (ex2_3 C T nat (\lambda (d:
 170 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0)))) (\lambda (d:
 171 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))))))
 172 (\lambda (H11: (eq A a3 a2)).(eq_ind A a2 (\lambda (_: A).((eq A a1 b) \to
 173 (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus
 174 O j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d
 175 u0 (asucc g b)))))))) (\lambda (H12: (eq A a1 b)).(eq_ind A b (\lambda (_:
 176 A).(ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
 177 (plus O j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
 178 nat).(arity g d u0 (asucc g b))))))) (eq_ind A a1 (\lambda (a4: A).(ex2_3 C T
 179 nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d
 180 c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
 181 (asucc g a4))))))) (ex2_3_intro C T nat (\lambda (d: C).(\lambda (_:
 182 T).(\lambda (j: nat).(drop (plus O j) O d c0)))) (\lambda (d: C).(\lambda
 183 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g a1))))) c0 u O (drop_refl
 184 c0) H0) b H12) a1 (sym_eq A a1 b H12))) a3 (sym_eq A a3 a2 H11))) a0 (sym_eq
 185 A a0 a1 H10))) H9)) H8)))) | (aprem_succ a0 a3 i0 H6 a4) \Rightarrow (\lambda
 186 (H7: (eq nat (S i0) O)).(\lambda (H8: (eq A (AHead a4 a0) (AHead a1
 187 a2))).(\lambda (H9: (eq A a3 b)).((let H10 \def (eq_ind nat (S i0) (\lambda
 188 (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
 189 False | (S _) \Rightarrow True])) I O H7) in (False_ind ((eq A (AHead a4 a0)
 190 (AHead a1 a2)) \to ((eq A a3 b) \to ((aprem i0 a0 a3) \to (ex2_3 C T nat
 191 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0))))
 192 (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
 193 b))))))))) H10)) H8 H9 H6))))]) in (H6 (refl_equal nat O) (refl_equal A
 194 (AHead a1 a2)) (refl_equal A b)))) | (S n) \Rightarrow (\lambda (H5: (aprem
 195 (S n) (AHead a1 a2) b)).(let H6 \def (match H5 in aprem return (\lambda (n0:
 196 nat).(\lambda (a0: A).(\lambda (a3: A).(\lambda (_: (aprem n0 a0 a3)).((eq
 197 nat n0 (S n)) \to ((eq A a0 (AHead a1 a2)) \to ((eq A a3 b) \to (ex2_3 C T
 198 nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus (S n) j) O
 199 d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
 200 (asucc g b))))))))))))) with [(aprem_zero a0 a3) \Rightarrow (\lambda (H6:
 201 (eq nat O (S n))).(\lambda (H7: (eq A (AHead a0 a3) (AHead a1 a2))).(\lambda
 202 (H8: (eq A a0 b)).((let H9 \def (eq_ind nat O (\lambda (e: nat).(match e in
 203 nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _)
 204 \Rightarrow False])) I (S n) H6) in (False_ind ((eq A (AHead a0 a3) (AHead a1
 205 a2)) \to ((eq A a0 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_:
 206 T).(\lambda (j: nat).(drop (plus (S n) j) O d c0)))) (\lambda (d: C).(\lambda
 207 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))))) H9)) H7 H8)))) |
 208 (aprem_succ a0 a3 i0 H6 a4) \Rightarrow (\lambda (H7: (eq nat (S i0) (S
 209 n))).(\lambda (H8: (eq A (AHead a4 a0) (AHead a1 a2))).(\lambda (H9: (eq A a3
 210 b)).((let H10 \def (f_equal nat nat (\lambda (e: nat).(match e in nat return
 211 (\lambda (_: nat).nat) with [O \Rightarrow i0 | (S n0) \Rightarrow n0])) (S
 212 i0) (S n) H7) in (eq_ind nat n (\lambda (n0: nat).((eq A (AHead a4 a0) (AHead
 213 a1 a2)) \to ((eq A a3 b) \to ((aprem n0 a0 a3) \to (ex2_3 C T nat (\lambda
 214 (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus (S n) j) O d c0))))
 215 (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
 216 b)))))))))) (\lambda (H11: (eq A (AHead a4 a0) (AHead a1 a2))).(let H12 \def
 217 (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with
 218 [(ASort _ _) \Rightarrow a0 | (AHead _ a5) \Rightarrow a5])) (AHead a4 a0)
 219 (AHead a1 a2) H11) in ((let H13 \def (f_equal A A (\lambda (e: A).(match e in
 220 A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a4 | (AHead a5 _)
 221 \Rightarrow a5])) (AHead a4 a0) (AHead a1 a2) H11) in (eq_ind A a1 (\lambda
 222 (_: A).((eq A a0 a2) \to ((eq A a3 b) \to ((aprem n a0 a3) \to (ex2_3 C T nat
 223 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus (S n) j) O d
 224 c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
 225 (asucc g b)))))))))) (\lambda (H14: (eq A a0 a2)).(eq_ind A a2 (\lambda (a5:
 226 A).((eq A a3 b) \to ((aprem n a5 a3) \to (ex2_3 C T nat (\lambda (d:
 227 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus (S n) j) O d c0)))) (\lambda
 228 (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))))))
 229 (\lambda (H15: (eq A a3 b)).(eq_ind A b (\lambda (a5: A).((aprem n a2 a5) \to
 230 (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus
 231 (S n) j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity
 232 g d u0 (asucc g b)))))))) (\lambda (H16: (aprem n a2 b)).(let H_x \def (H3 n
 233 b H16) in (let H17 \def H_x in (ex2_3_ind C T nat (\lambda (d: C).(\lambda
 234 (_: T).(\lambda (j: nat).(drop (plus n j) O d (CHead c0 (Bind Abst) u)))))
 235 (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
 236 b))))) (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
 237 (plus (S n) j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
 238 nat).(arity g d u0 (asucc g b)))))) (\lambda (x0: C).(\lambda (x1:
 239 T).(\lambda (x2: nat).(\lambda (H18: (drop (plus n x2) O x0 (CHead c0 (Bind
 240 Abst) u))).(\lambda (H19: (arity g x0 x1 (asucc g b))).(ex2_3_intro C T nat
 241 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus (S n) j) O d
 242 c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
 243 (asucc g b))))) x0 x1 x2 (drop_S Abst x0 c0 u (plus n x2) H18) H19))))))
 244 H17)))) a3 (sym_eq A a3 b H15))) a0 (sym_eq A a0 a2 H14))) a4 (sym_eq A a4 a1
 245 H13))) H12))) i0 (sym_eq nat i0 n H10))) H8 H9 H6))))]) in (H6 (refl_equal
 246 nat (S n)) (refl_equal A (AHead a1 a2)) (refl_equal A b))))]) H4)))))))))))))
 247 (\lambda (c0: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u
 248 a1)).(\lambda (_: ((\forall (i: nat).(\forall (b: A).((aprem i a1 b) \to
 249 (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus
 250 i j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d
 251 u0 (asucc g b))))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_:
 252 (arity g c0 t0 (AHead a1 a2))).(\lambda (H3: ((\forall (i: nat).(\forall (b:
 253 A).((aprem i (AHead a1 a2) b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_:
 254 T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda
 255 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))))).(\lambda (i:
 256 nat).(\lambda (b: A).(\lambda (H4: (aprem i a2 b)).(let H5 \def (H3 (S i) b
 257 (aprem_succ a2 b i H4 a1)) in (ex2_3_ind C T nat (\lambda (d: C).(\lambda (_:
 258 T).(\lambda (j: nat).(drop (S (plus i j)) O d c0)))) (\lambda (d: C).(\lambda
 259 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b))))) (ex2_3 C T nat
 260 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0))))
 261 (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
 262 b)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: nat).(\lambda (H6:
 263 (drop (S (plus i x2)) O x0 c0)).(\lambda (H7: (arity g x0 x1 (asucc g
 264 b))).(C_ind (\lambda (c1: C).((drop (S (plus i x2)) O c1 c0) \to ((arity g c1
 265 x1 (asucc g b)) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda
 266 (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0:
 267 T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))) (\lambda (n:
 268 nat).(\lambda (H8: (drop (S (plus i x2)) O (CSort n) c0)).(\lambda (_: (arity
 269 g (CSort n) x1 (asucc g b))).(and3_ind (eq C c0 (CSort n)) (eq nat (S (plus i
 270 x2)) O) (eq nat O O) (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda
 271 (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0:
 272 T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))) (\lambda (_: (eq C c0
 273 (CSort n))).(\lambda (H11: (eq nat (S (plus i x2)) O)).(\lambda (_: (eq nat O
 274 O)).(let H13 \def (eq_ind nat (S (plus i x2)) (\lambda (ee: nat).(match ee in
 275 nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
 276 \Rightarrow True])) I O H11) in (False_ind (ex2_3 C T nat (\lambda (d:
 277 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d:
 278 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))) H13)))))
 279 (drop_gen_sort n (S (plus i x2)) O c0 H8))))) (\lambda (d: C).(\lambda (IHd:
 280 (((drop (S (plus i x2)) O d c0) \to ((arity g d x1 (asucc g b)) \to (ex2_3 C
 281 T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O
 282 d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
 283 (asucc g b)))))))))).(\lambda (k: K).(\lambda (t1: T).(\lambda (H8: (drop (S
 284 (plus i x2)) O (CHead d k t1) c0)).(\lambda (H9: (arity g (CHead d k t1) x1
 285 (asucc g b))).((match k in K return (\lambda (k0: K).((arity g (CHead d k0
 286 t1) x1 (asucc g b)) \to ((drop (r k0 (plus i x2)) O d c0) \to (ex2_3 C T nat
 287 (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d0
 288 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
 289 (asucc g b))))))))) with [(Bind b0) \Rightarrow (\lambda (H10: (arity g
 290 (CHead d (Bind b0) t1) x1 (asucc g b))).(\lambda (H11: (drop (r (Bind b0)
 291 (plus i x2)) O d c0)).(ex2_3_intro C T nat (\lambda (d0: C).(\lambda (_:
 292 T).(\lambda (j: nat).(drop (plus i j) O d0 c0)))) (\lambda (d0: C).(\lambda
 293 (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))) (CHead d (Bind b0)
 294 t1) x1 (S x2) (eq_ind nat (S (plus i x2)) (\lambda (n: nat).(drop n O (CHead
 295 d (Bind b0) t1) c0)) (drop_drop (Bind b0) (plus i x2) d c0 H11 t1) (plus i (S
 296 x2)) (plus_n_Sm i x2)) H10))) | (Flat f) \Rightarrow (\lambda (H10: (arity g
 297 (CHead d (Flat f) t1) x1 (asucc g b))).(\lambda (H11: (drop (r (Flat f) (plus
 298 i x2)) O d c0)).(let H12 \def (IHd H11 (arity_cimp_conf g (CHead d (Flat f)
 299 t1) x1 (asucc g b) H10 d (cimp_flat_sx f d t1))) in (ex2_3_ind C T nat
 300 (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d0
 301 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
 302 (asucc g b))))) (ex2_3 C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
 303 nat).(drop (plus i j) O d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda
 304 (_: nat).(arity g d0 u0 (asucc g b)))))) (\lambda (x3: C).(\lambda (x4:
 305 T).(\lambda (x5: nat).(\lambda (H13: (drop (plus i x5) O x3 c0)).(\lambda
 306 (H14: (arity g x3 x4 (asucc g b))).(ex2_3_intro C T nat (\lambda (d0:
 307 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d0 c0)))) (\lambda
 308 (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))) x3
 309 x4 x5 H13 H14)))))) H12))))]) H9 (drop_gen_drop k d c0 t1 (plus i x2)
 310 H8)))))))) x0 H6 H7)))))) H5)))))))))))))) (\lambda (c0: C).(\lambda (u:
 311 T).(\lambda (a0: A).(\lambda (_: (arity g c0 u (asucc g a0))).(\lambda (_:
 312 ((\forall (i: nat).(\forall (b: A).((aprem i (asucc g a0) b) \to (ex2_3 C T
 313 nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d
 314 c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
 315 (asucc g b))))))))))).(\lambda (t0: T).(\lambda (_: (arity g c0 t0
 316 a0)).(\lambda (H3: ((\forall (i: nat).(\forall (b: A).((aprem i a0 b) \to
 317 (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus
 318 i j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d
 319 u0 (asucc g b))))))))))).(\lambda (i: nat).(\lambda (b: A).(\lambda (H4:
 320 (aprem i a0 b)).(let H_x \def (H3 i b H4) in (let H5 \def H_x in (ex2_3_ind C
 321 T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d
 322 c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
 323 (asucc g b))))) (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
 324 nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda
 325 (_: nat).(arity g d u0 (asucc g b)))))) (\lambda (x0: C).(\lambda (x1:
 326 T).(\lambda (x2: nat).(\lambda (H6: (drop (plus i x2) O x0 c0)).(\lambda (H7:
 327 (arity g x0 x1 (asucc g b))).(ex2_3_intro C T nat (\lambda (d: C).(\lambda
 328 (_: T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda
 329 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b))))) x0 x1 x2 H6 H7))))))
 330 H5)))))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda
 331 (_: (arity g c0 t0 a1)).(\lambda (H1: ((\forall (i: nat).(\forall (b:
 332 A).((aprem i a1 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_:
 333 T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u:
 334 T).(\lambda (_: nat).(arity g d u (asucc g b))))))))))).(\lambda (a2:
 335 A).(\lambda (H2: (leq g a1 a2)).(\lambda (i: nat).(\lambda (b: A).(\lambda
 336 (H3: (aprem i a2 b)).(let H_x \def (aprem_repl g a1 a2 H2 i b H3) in (let H4
 337 \def H_x in (ex2_ind A (\lambda (b1: A).(leq g b1 b)) (\lambda (b1: A).(aprem
 338 i a1 b1)) (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
 339 nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_:
 340 nat).(arity g d u (asucc g b)))))) (\lambda (x: A).(\lambda (H5: (leq g x
 341 b)).(\lambda (H6: (aprem i a1 x)).(let H_x0 \def (H1 i x H6) in (let H7 \def
 342 H_x0 in (ex2_3_ind C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
 343 nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_:
 344 nat).(arity g d u (asucc g x))))) (ex2_3 C T nat (\lambda (d: C).(\lambda (_:
 345 T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u:
 346 T).(\lambda (_: nat).(arity g d u (asucc g b)))))) (\lambda (x0: C).(\lambda
 347 (x1: T).(\lambda (x2: nat).(\lambda (H8: (drop (plus i x2) O x0 c0)).(\lambda
 348 (H9: (arity g x0 x1 (asucc g x))).(ex2_3_intro C T nat (\lambda (d:
 349 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d:
 350 C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc g b))))) x0 x1 x2 H8
 351 (arity_repl g x0 x1 (asucc g x) H9 (asucc g b) (asucc_repl g x b H5))))))))
 352 H7)))))) H4))))))))))))) c t a H))))).
 353