-(aprem O (AHead a1 a2) b)).(let H6 \def (match H5 in aprem return (\lambda
-(n: nat).(\lambda (a0: A).(\lambda (a3: A).(\lambda (_: (aprem n a0 a3)).((eq
-nat n O) \to ((eq A a0 (AHead a1 a2)) \to ((eq A a3 b) \to (ex2_3 C T nat
-(\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0))))
-(\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
-b))))))))))))) with [(aprem_zero a0 a3) \Rightarrow (\lambda (_: (eq nat O
-O)).(\lambda (H7: (eq A (AHead a0 a3) (AHead a1 a2))).(\lambda (H8: (eq A a0
-b)).((let H9 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda
-(_: A).A) with [(ASort _ _) \Rightarrow a3 | (AHead _ a4) \Rightarrow a4]))
-(AHead a0 a3) (AHead a1 a2) H7) in ((let H10 \def (f_equal A A (\lambda (e:
-A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a0 |
-(AHead a4 _) \Rightarrow a4])) (AHead a0 a3) (AHead a1 a2) H7) in (eq_ind A
-a1 (\lambda (a4: A).((eq A a3 a2) \to ((eq A a4 b) \to (ex2_3 C T nat
-(\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0))))
-(\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
-b))))))))) (\lambda (H11: (eq A a3 a2)).(eq_ind A a2 (\lambda (_: A).((eq A
-a1 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
-nat).(drop (plus O j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda
-(_: nat).(arity g d u0 (asucc g b)))))))) (\lambda (H12: (eq A a1 b)).(eq_ind
-A b (\lambda (_: A).(ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda
-(j: nat).(drop (plus O j) O d c0)))) (\lambda (d: C).(\lambda (u0:
-T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))) (eq_ind A a1 (\lambda
-(a4: A).(ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
-nat).(drop (plus O j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda
-(_: nat).(arity g d u0 (asucc g a4))))))) (ex2_3_intro C T nat (\lambda (d:
-C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0)))) (\lambda (d:
-C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g a1))))) c0 u O
-(drop_refl c0) H0) b H12) a1 (sym_eq A a1 b H12))) a3 (sym_eq A a3 a2 H11)))
-a0 (sym_eq A a0 a1 H10))) H9)) H8)))) | (aprem_succ a0 a3 i0 H6 a4)
-\Rightarrow (\lambda (H7: (eq nat (S i0) O)).(\lambda (H8: (eq A (AHead a4
-a0) (AHead a1 a2))).(\lambda (H9: (eq A a3 b)).((let H10 \def (eq_ind nat (S
-i0) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
-\Rightarrow False | (S _) \Rightarrow True])) I O H7) in (False_ind ((eq A
-(AHead a4 a0) (AHead a1 a2)) \to ((eq A a3 b) \to ((aprem i0 a0 a3) \to
-(ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus
-O j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d
-u0 (asucc g b))))))))) H10)) H8 H9 H6))))]) in (H6 (refl_equal nat O)
-(refl_equal A (AHead a1 a2)) (refl_equal A b)))) (\lambda (i0: nat).(\lambda
-(_: (((aprem i0 (AHead a1 a2) b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda
-(_: T).(\lambda (j: nat).(drop (plus i0 j) O d c0)))) (\lambda (d:
-C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
-b))))))))).(\lambda (H5: (aprem (S i0) (AHead a1 a2) b)).(let H6 \def (match
-H5 in aprem return (\lambda (n: nat).(\lambda (a0: A).(\lambda (a3:
-A).(\lambda (_: (aprem n a0 a3)).((eq nat n (S i0)) \to ((eq A a0 (AHead a1
-a2)) \to ((eq A a3 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_:
-T).(\lambda (j: nat).(drop (plus (S i0) j) O d c0)))) (\lambda (d:
-C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))))))))))
-with [(aprem_zero a0 a3) \Rightarrow (\lambda (H6: (eq nat O (S
-i0))).(\lambda (H7: (eq A (AHead a0 a3) (AHead a1 a2))).(\lambda (H8: (eq A
-a0 b)).((let H9 \def (eq_ind nat O (\lambda (e: nat).(match e in nat return
-(\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
-I (S i0) H6) in (False_ind ((eq A (AHead a0 a3) (AHead a1 a2)) \to ((eq A a0
-b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
-(plus (S i0) j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
-nat).(arity g d u0 (asucc g b)))))))) H9)) H7 H8)))) | (aprem_succ a0 a3 i1
-H6 a4) \Rightarrow (\lambda (H7: (eq nat (S i1) (S i0))).(\lambda (H8: (eq A
-(AHead a4 a0) (AHead a1 a2))).(\lambda (H9: (eq A a3 b)).((let H10 \def
-(f_equal nat nat (\lambda (e: nat).(match e in nat return (\lambda (_:
-nat).nat) with [O \Rightarrow i1 | (S n) \Rightarrow n])) (S i1) (S i0) H7)
-in (eq_ind nat i0 (\lambda (n: nat).((eq A (AHead a4 a0) (AHead a1 a2)) \to
-((eq A a3 b) \to ((aprem n a0 a3) \to (ex2_3 C T nat (\lambda (d: C).(\lambda
-(_: T).(\lambda (j: nat).(drop (plus (S i0) j) O d c0)))) (\lambda (d:
-C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))))
-(\lambda (H11: (eq A (AHead a4 a0) (AHead a1 a2))).(let H12 \def (f_equal A A
-(\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _)
-\Rightarrow a0 | (AHead _ a5) \Rightarrow a5])) (AHead a4 a0) (AHead a1 a2)
-H11) in ((let H13 \def (f_equal A A (\lambda (e: A).(match e in A return
-(\lambda (_: A).A) with [(ASort _ _) \Rightarrow a4 | (AHead a5 _)
-\Rightarrow a5])) (AHead a4 a0) (AHead a1 a2) H11) in (eq_ind A a1 (\lambda
-(_: A).((eq A a0 a2) \to ((eq A a3 b) \to ((aprem i0 a0 a3) \to (ex2_3 C T
-nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus (S i0) j) O
-d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
-(asucc g b)))))))))) (\lambda (H14: (eq A a0 a2)).(eq_ind A a2 (\lambda (a5:
-A).((eq A a3 b) \to ((aprem i0 a5 a3) \to (ex2_3 C T nat (\lambda (d:
-C).(\lambda (_: T).(\lambda (j: nat).(drop (plus (S i0) j) O d c0))))