(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0".
+include "LambdaDelta-1/ty3/pr3_props.ma".
-include "ty3/pr3_props.ma".
-
-include "tau0/defs.ma".
+include "LambdaDelta-1/tau0/defs.ma".
theorem ty3_tau0:
\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u
(b: B).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (ty3 g (CHead c0 (Bind
b) u0) t2 t3)).(\lambda (H3: ((\forall (t4: T).((tau0 g (CHead c0 (Bind b)
u0) t2 t4) \to (ty3 g (CHead c0 (Bind b) u0) t2 t4))))).(\lambda (t0:
-T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u0) t3 t0)).(\lambda (_: ((\forall
-(t4: T).((tau0 g (CHead c0 (Bind b) u0) t3 t4) \to (ty3 g (CHead c0 (Bind b)
-u0) t3 t4))))).(\lambda (t4: T).(\lambda (H6: (tau0 g c0 (THead (Bind b) u0
-t2) t4)).(let H7 \def (match H6 in tau0 return (\lambda (c1: C).(\lambda (t5:
-T).(\lambda (t6: T).(\lambda (_: (tau0 ? c1 t5 t6)).((eq C c1 c0) \to ((eq T
-t5 (THead (Bind b) u0 t2)) \to ((eq T t6 t4) \to (ty3 g c0 (THead (Bind b) u0
-t2) t4)))))))) with [(tau0_sort c1 n) \Rightarrow (\lambda (H7: (eq C c1
-c0)).(\lambda (H8: (eq T (TSort n) (THead (Bind b) u0 t2))).(\lambda (H9: (eq
-T (TSort (next g n)) t4)).(eq_ind C c0 (\lambda (_: C).((eq T (TSort n)
-(THead (Bind b) u0 t2)) \to ((eq T (TSort (next g n)) t4) \to (ty3 g c0
-(THead (Bind b) u0 t2) t4)))) (\lambda (H10: (eq T (TSort n) (THead (Bind b)
-u0 t2))).(let H11 \def (eq_ind T (TSort n) (\lambda (e: T).(match e in T
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
-\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u0
-t2) H10) in (False_ind ((eq T (TSort (next g n)) t4) \to (ty3 g c0 (THead
-(Bind b) u0 t2) t4)) H11))) c1 (sym_eq C c1 c0 H7) H8 H9)))) | (tau0_abbr c1
-d v i H7 w H8) \Rightarrow (\lambda (H9: (eq C c1 c0)).(\lambda (H10: (eq T
-(TLRef i) (THead (Bind b) u0 t2))).(\lambda (H11: (eq T (lift (S i) O w)
-t4)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef i) (THead (Bind b) u0 t2))
-\to ((eq T (lift (S i) O w) t4) \to ((getl i c2 (CHead d (Bind Abbr) v)) \to
-((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0 t2) t4)))))) (\lambda (H12:
-(eq T (TLRef i) (THead (Bind b) u0 t2))).(let H13 \def (eq_ind T (TLRef i)
-(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
-\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
-False])) I (THead (Bind b) u0 t2) H12) in (False_ind ((eq T (lift (S i) O w)
-t4) \to ((getl i c0 (CHead d (Bind Abbr) v)) \to ((tau0 g d v w) \to (ty3 g
-c0 (THead (Bind b) u0 t2) t4)))) H13))) c1 (sym_eq C c1 c0 H9) H10 H11 H7
-H8)))) | (tau0_abst c1 d v i H7 w H8) \Rightarrow (\lambda (H9: (eq C c1
-c0)).(\lambda (H10: (eq T (TLRef i) (THead (Bind b) u0 t2))).(\lambda (H11:
-(eq T (lift (S i) O v) t4)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef i)
-(THead (Bind b) u0 t2)) \to ((eq T (lift (S i) O v) t4) \to ((getl i c2
-(CHead d (Bind Abst) v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0
-t2) t4)))))) (\lambda (H12: (eq T (TLRef i) (THead (Bind b) u0 t2))).(let H13
+T).(\lambda (H4: (tau0 g c0 (THead (Bind b) u0 t2) t0)).(let H5 \def (match
+H4 in tau0 return (\lambda (c1: C).(\lambda (t4: T).(\lambda (t5: T).(\lambda
+(_: (tau0 ? c1 t4 t5)).((eq C c1 c0) \to ((eq T t4 (THead (Bind b) u0 t2))
+\to ((eq T t5 t0) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))))))) with
+[(tau0_sort c1 n) \Rightarrow (\lambda (H5: (eq C c1 c0)).(\lambda (H6: (eq T
+(TSort n) (THead (Bind b) u0 t2))).(\lambda (H7: (eq T (TSort (next g n))
+t0)).(eq_ind C c0 (\lambda (_: C).((eq T (TSort n) (THead (Bind b) u0 t2))
+\to ((eq T (TSort (next g n)) t0) \to (ty3 g c0 (THead (Bind b) u0 t2) t0))))
+(\lambda (H8: (eq T (TSort n) (THead (Bind b) u0 t2))).(let H9 \def (eq_ind T
+(TSort n) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
+[(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _)
+\Rightarrow False])) I (THead (Bind b) u0 t2) H8) in (False_ind ((eq T (TSort
+(next g n)) t0) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)) H9))) c1 (sym_eq C
+c1 c0 H5) H6 H7)))) | (tau0_abbr c1 d v i H5 w H6) \Rightarrow (\lambda (H7:
+(eq C c1 c0)).(\lambda (H8: (eq T (TLRef i) (THead (Bind b) u0 t2))).(\lambda
+(H9: (eq T (lift (S i) O w) t0)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef
+i) (THead (Bind b) u0 t2)) \to ((eq T (lift (S i) O w) t0) \to ((getl i c2
+(CHead d (Bind Abbr) v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0
+t2) t0)))))) (\lambda (H10: (eq T (TLRef i) (THead (Bind b) u0 t2))).(let H11
\def (eq_ind T (TLRef i) (\lambda (e: T).(match e in T return (\lambda (_:
T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
-(THead _ _ _) \Rightarrow False])) I (THead (Bind b) u0 t2) H12) in
-(False_ind ((eq T (lift (S i) O v) t4) \to ((getl i c0 (CHead d (Bind Abst)
-v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0 t2) t4)))) H13))) c1
-(sym_eq C c1 c0 H9) H10 H11 H7 H8)))) | (tau0_bind b0 c1 v t5 t6 H7)
-\Rightarrow (\lambda (H8: (eq C c1 c0)).(\lambda (H9: (eq T (THead (Bind b0)
-v t5) (THead (Bind b) u0 t2))).(\lambda (H10: (eq T (THead (Bind b0) v t6)
-t4)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead (Bind b0) v t5) (THead (Bind
-b) u0 t2)) \to ((eq T (THead (Bind b0) v t6) t4) \to ((tau0 g (CHead c2 (Bind
-b0) v) t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t4))))) (\lambda (H11: (eq
-T (THead (Bind b0) v t5) (THead (Bind b) u0 t2))).(let H12 \def (f_equal T T
-(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
-\Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7) \Rightarrow t7]))
-(THead (Bind b0) v t5) (THead (Bind b) u0 t2) H11) in ((let H13 \def (f_equal
-T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
-\Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t7 _) \Rightarrow t7]))
-(THead (Bind b0) v t5) (THead (Bind b) u0 t2) H11) in ((let H14 \def (f_equal
-T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with [(TSort _)
-\Rightarrow b0 | (TLRef _) \Rightarrow b0 | (THead k _ _) \Rightarrow (match
-k in K return (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | (Flat _)
-\Rightarrow b0])])) (THead (Bind b0) v t5) (THead (Bind b) u0 t2) H11) in
-(eq_ind B b (\lambda (b1: B).((eq T v u0) \to ((eq T t5 t2) \to ((eq T (THead
-(Bind b1) v t6) t4) \to ((tau0 g (CHead c0 (Bind b1) v) t5 t6) \to (ty3 g c0
-(THead (Bind b) u0 t2) t4)))))) (\lambda (H15: (eq T v u0)).(eq_ind T u0
-(\lambda (t7: T).((eq T t5 t2) \to ((eq T (THead (Bind b) t7 t6) t4) \to
-((tau0 g (CHead c0 (Bind b) t7) t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2)
-t4))))) (\lambda (H16: (eq T t5 t2)).(eq_ind T t2 (\lambda (t7: T).((eq T
-(THead (Bind b) u0 t6) t4) \to ((tau0 g (CHead c0 (Bind b) u0) t7 t6) \to
-(ty3 g c0 (THead (Bind b) u0 t2) t4)))) (\lambda (H17: (eq T (THead (Bind b)
-u0 t6) t4)).(eq_ind T (THead (Bind b) u0 t6) (\lambda (t7: T).((tau0 g (CHead
-c0 (Bind b) u0) t2 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t7))) (\lambda
-(H18: (tau0 g (CHead c0 (Bind b) u0) t2 t6)).(let H_y \def (H3 t6 H18) in
-(ex_ind T (\lambda (t7: T).(ty3 g (CHead c0 (Bind b) u0) t6 t7)) (ty3 g c0
-(THead (Bind b) u0 t2) (THead (Bind b) u0 t6)) (\lambda (x: T).(\lambda (H19:
-(ty3 g (CHead c0 (Bind b) u0) t6 x)).(ty3_bind g c0 u0 t H0 b t2 t6 H_y x
-H19))) (ty3_correct g (CHead c0 (Bind b) u0) t2 t6 H_y)))) t4 H17)) t5
-(sym_eq T t5 t2 H16))) v (sym_eq T v u0 H15))) b0 (sym_eq B b0 b H14))) H13))
-H12))) c1 (sym_eq C c1 c0 H8) H9 H10 H7)))) | (tau0_appl c1 v t5 t6 H7)
-\Rightarrow (\lambda (H8: (eq C c1 c0)).(\lambda (H9: (eq T (THead (Flat
-Appl) v t5) (THead (Bind b) u0 t2))).(\lambda (H10: (eq T (THead (Flat Appl)
-v t6) t4)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead (Flat Appl) v t5)
-(THead (Bind b) u0 t2)) \to ((eq T (THead (Flat Appl) v t6) t4) \to ((tau0 g
-c2 t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t4))))) (\lambda (H11: (eq T
-(THead (Flat Appl) v t5) (THead (Bind b) u0 t2))).(let H12 \def (eq_ind T
-(THead (Flat Appl) v t5) (\lambda (e: T).(match e in T return (\lambda (_:
+(THead _ _ _) \Rightarrow False])) I (THead (Bind b) u0 t2) H10) in
+(False_ind ((eq T (lift (S i) O w) t0) \to ((getl i c0 (CHead d (Bind Abbr)
+v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))) H11))) c1
+(sym_eq C c1 c0 H7) H8 H9 H5 H6)))) | (tau0_abst c1 d v i H5 w H6)
+\Rightarrow (\lambda (H7: (eq C c1 c0)).(\lambda (H8: (eq T (TLRef i) (THead
+(Bind b) u0 t2))).(\lambda (H9: (eq T (lift (S i) O v) t0)).(eq_ind C c0
+(\lambda (c2: C).((eq T (TLRef i) (THead (Bind b) u0 t2)) \to ((eq T (lift (S
+i) O v) t0) \to ((getl i c2 (CHead d (Bind Abst) v)) \to ((tau0 g d v w) \to
+(ty3 g c0 (THead (Bind b) u0 t2) t0)))))) (\lambda (H10: (eq T (TLRef i)
+(THead (Bind b) u0 t2))).(let H11 \def (eq_ind T (TLRef i) (\lambda (e:
+T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
+False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
+(THead (Bind b) u0 t2) H10) in (False_ind ((eq T (lift (S i) O v) t0) \to
+((getl i c0 (CHead d (Bind Abst) v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead
+(Bind b) u0 t2) t0)))) H11))) c1 (sym_eq C c1 c0 H7) H8 H9 H5 H6)))) |
+(tau0_bind b0 c1 v t4 t5 H5) \Rightarrow (\lambda (H6: (eq C c1 c0)).(\lambda
+(H7: (eq T (THead (Bind b0) v t4) (THead (Bind b) u0 t2))).(\lambda (H8: (eq
+T (THead (Bind b0) v t5) t0)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead
+(Bind b0) v t4) (THead (Bind b) u0 t2)) \to ((eq T (THead (Bind b0) v t5) t0)
+\to ((tau0 g (CHead c2 (Bind b0) v) t4 t5) \to (ty3 g c0 (THead (Bind b) u0
+t2) t0))))) (\lambda (H9: (eq T (THead (Bind b0) v t4) (THead (Bind b) u0
+t2))).(let H10 \def (f_equal T T (\lambda (e: T).(match e in T return
+(\lambda (_: T).T) with [(TSort _) \Rightarrow t4 | (TLRef _) \Rightarrow t4
+| (THead _ _ t6) \Rightarrow t6])) (THead (Bind b0) v t4) (THead (Bind b) u0
+t2) H9) in ((let H11 \def (f_equal T T (\lambda (e: T).(match e in T return
+(\lambda (_: T).T) with [(TSort _) \Rightarrow v | (TLRef _) \Rightarrow v |
+(THead _ t6 _) \Rightarrow t6])) (THead (Bind b0) v t4) (THead (Bind b) u0
+t2) H9) in ((let H12 \def (f_equal T B (\lambda (e: T).(match e in T return
+(\lambda (_: T).B) with [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0
+| (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).B) with
+[(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) (THead (Bind b0) v
+t4) (THead (Bind b) u0 t2) H9) in (eq_ind B b (\lambda (b1: B).((eq T v u0)
+\to ((eq T t4 t2) \to ((eq T (THead (Bind b1) v t5) t0) \to ((tau0 g (CHead
+c0 (Bind b1) v) t4 t5) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))))) (\lambda
+(H13: (eq T v u0)).(eq_ind T u0 (\lambda (t6: T).((eq T t4 t2) \to ((eq T
+(THead (Bind b) t6 t5) t0) \to ((tau0 g (CHead c0 (Bind b) t6) t4 t5) \to
+(ty3 g c0 (THead (Bind b) u0 t2) t0))))) (\lambda (H14: (eq T t4 t2)).(eq_ind
+T t2 (\lambda (t6: T).((eq T (THead (Bind b) u0 t5) t0) \to ((tau0 g (CHead
+c0 (Bind b) u0) t6 t5) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))) (\lambda
+(H15: (eq T (THead (Bind b) u0 t5) t0)).(eq_ind T (THead (Bind b) u0 t5)
+(\lambda (t6: T).((tau0 g (CHead c0 (Bind b) u0) t2 t5) \to (ty3 g c0 (THead
+(Bind b) u0 t2) t6))) (\lambda (H16: (tau0 g (CHead c0 (Bind b) u0) t2
+t5)).(ty3_bind g c0 u0 t H0 b t2 t5 (H3 t5 H16))) t0 H15)) t4 (sym_eq T t4 t2
+H14))) v (sym_eq T v u0 H13))) b0 (sym_eq B b0 b H12))) H11)) H10))) c1
+(sym_eq C c1 c0 H6) H7 H8 H5)))) | (tau0_appl c1 v t4 t5 H5) \Rightarrow
+(\lambda (H6: (eq C c1 c0)).(\lambda (H7: (eq T (THead (Flat Appl) v t4)
+(THead (Bind b) u0 t2))).(\lambda (H8: (eq T (THead (Flat Appl) v t5)
+t0)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead (Flat Appl) v t4) (THead
+(Bind b) u0 t2)) \to ((eq T (THead (Flat Appl) v t5) t0) \to ((tau0 g c2 t4
+t5) \to (ty3 g c0 (THead (Bind b) u0 t2) t0))))) (\lambda (H9: (eq T (THead
+(Flat Appl) v t4) (THead (Bind b) u0 t2))).(let H10 \def (eq_ind T (THead
+(Flat Appl) v t4) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop)
+with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _
+_) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
+\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) u0 t2)
+H9) in (False_ind ((eq T (THead (Flat Appl) v t5) t0) \to ((tau0 g c0 t4 t5)
+\to (ty3 g c0 (THead (Bind b) u0 t2) t0))) H10))) c1 (sym_eq C c1 c0 H6) H7
+H8 H5)))) | (tau0_cast c1 v1 v2 H5 t4 t5 H6) \Rightarrow (\lambda (H7: (eq C
+c1 c0)).(\lambda (H8: (eq T (THead (Flat Cast) v1 t4) (THead (Bind b) u0
+t2))).(\lambda (H9: (eq T (THead (Flat Cast) v2 t5) t0)).(eq_ind C c0
+(\lambda (c2: C).((eq T (THead (Flat Cast) v1 t4) (THead (Bind b) u0 t2)) \to
+((eq T (THead (Flat Cast) v2 t5) t0) \to ((tau0 g c2 v1 v2) \to ((tau0 g c2
+t4 t5) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))))) (\lambda (H10: (eq T
+(THead (Flat Cast) v1 t4) (THead (Bind b) u0 t2))).(let H11 \def (eq_ind T
+(THead (Flat Cast) v1 t4) (\lambda (e: T).(match e in T return (\lambda (_:
T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
[(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind
-b) u0 t2) H11) in (False_ind ((eq T (THead (Flat Appl) v t6) t4) \to ((tau0 g
-c0 t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t4))) H12))) c1 (sym_eq C c1
-c0 H8) H9 H10 H7)))) | (tau0_cast c1 v1 v2 H7 t5 t6 H8) \Rightarrow (\lambda
-(H9: (eq C c1 c0)).(\lambda (H10: (eq T (THead (Flat Cast) v1 t5) (THead
-(Bind b) u0 t2))).(\lambda (H11: (eq T (THead (Flat Cast) v2 t6) t4)).(eq_ind
-C c0 (\lambda (c2: C).((eq T (THead (Flat Cast) v1 t5) (THead (Bind b) u0
-t2)) \to ((eq T (THead (Flat Cast) v2 t6) t4) \to ((tau0 g c2 v1 v2) \to
-((tau0 g c2 t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t4)))))) (\lambda
-(H12: (eq T (THead (Flat Cast) v1 t5) (THead (Bind b) u0 t2))).(let H13 \def
-(eq_ind T (THead (Flat Cast) v1 t5) (\lambda (e: T).(match e in T return
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
-\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
-(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
-True])])) I (THead (Bind b) u0 t2) H12) in (False_ind ((eq T (THead (Flat
-Cast) v2 t6) t4) \to ((tau0 g c0 v1 v2) \to ((tau0 g c0 t5 t6) \to (ty3 g c0
-(THead (Bind b) u0 t2) t4)))) H13))) c1 (sym_eq C c1 c0 H9) H10 H11 H7
-H8))))]) in (H7 (refl_equal C c0) (refl_equal T (THead (Bind b) u0 t2))
-(refl_equal T t4)))))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda
-(u0: T).(\lambda (H0: (ty3 g c0 w u0)).(\lambda (_: ((\forall (t2: T).((tau0
-g c0 w t2) \to (ty3 g c0 w t2))))).(\lambda (v: T).(\lambda (t: T).(\lambda
-(H2: (ty3 g c0 v (THead (Bind Abst) u0 t))).(\lambda (H3: ((\forall (t2:
-T).((tau0 g c0 v t2) \to (ty3 g c0 v t2))))).(\lambda (t2: T).(\lambda (H4:
-(tau0 g c0 (THead (Flat Appl) w v) t2)).(let H5 \def (match H4 in tau0 return
-(\lambda (c1: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (tau0 ? c1 t0
-t3)).((eq C c1 c0) \to ((eq T t0 (THead (Flat Appl) w v)) \to ((eq T t3 t2)
-\to (ty3 g c0 (THead (Flat Appl) w v) t2)))))))) with [(tau0_sort c1 n)
-\Rightarrow (\lambda (H5: (eq C c1 c0)).(\lambda (H6: (eq T (TSort n) (THead
-(Flat Appl) w v))).(\lambda (H7: (eq T (TSort (next g n)) t2)).(eq_ind C c0
-(\lambda (_: C).((eq T (TSort n) (THead (Flat Appl) w v)) \to ((eq T (TSort
-(next g n)) t2) \to (ty3 g c0 (THead (Flat Appl) w v) t2)))) (\lambda (H8:
-(eq T (TSort n) (THead (Flat Appl) w v))).(let H9 \def (eq_ind T (TSort n)
-(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
-\Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
-False])) I (THead (Flat Appl) w v) H8) in (False_ind ((eq T (TSort (next g
-n)) t2) \to (ty3 g c0 (THead (Flat Appl) w v) t2)) H9))) c1 (sym_eq C c1 c0
-H5) H6 H7)))) | (tau0_abbr c1 d v0 i H5 w0 H6) \Rightarrow (\lambda (H7: (eq
-C c1 c0)).(\lambda (H8: (eq T (TLRef i) (THead (Flat Appl) w v))).(\lambda
-(H9: (eq T (lift (S i) O w0) t2)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef
-i) (THead (Flat Appl) w v)) \to ((eq T (lift (S i) O w0) t2) \to ((getl i c2
+b) u0 t2) H10) in (False_ind ((eq T (THead (Flat Cast) v2 t5) t0) \to ((tau0
+g c0 v1 v2) \to ((tau0 g c0 t4 t5) \to (ty3 g c0 (THead (Bind b) u0 t2)
+t0)))) H11))) c1 (sym_eq C c1 c0 H7) H8 H9 H5 H6))))]) in (H5 (refl_equal C
+c0) (refl_equal T (THead (Bind b) u0 t2)) (refl_equal T t0)))))))))))))))
+(\lambda (c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda (H0: (ty3 g c0 w
+u0)).(\lambda (_: ((\forall (t2: T).((tau0 g c0 w t2) \to (ty3 g c0 w
+t2))))).(\lambda (v: T).(\lambda (t: T).(\lambda (H2: (ty3 g c0 v (THead
+(Bind Abst) u0 t))).(\lambda (H3: ((\forall (t2: T).((tau0 g c0 v t2) \to
+(ty3 g c0 v t2))))).(\lambda (t2: T).(\lambda (H4: (tau0 g c0 (THead (Flat
+Appl) w v) t2)).(let H5 \def (match H4 in tau0 return (\lambda (c1:
+C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (tau0 ? c1 t0 t3)).((eq C
+c1 c0) \to ((eq T t0 (THead (Flat Appl) w v)) \to ((eq T t3 t2) \to (ty3 g c0
+(THead (Flat Appl) w v) t2)))))))) with [(tau0_sort c1 n) \Rightarrow
+(\lambda (H5: (eq C c1 c0)).(\lambda (H6: (eq T (TSort n) (THead (Flat Appl)
+w v))).(\lambda (H7: (eq T (TSort (next g n)) t2)).(eq_ind C c0 (\lambda (_:
+C).((eq T (TSort n) (THead (Flat Appl) w v)) \to ((eq T (TSort (next g n))
+t2) \to (ty3 g c0 (THead (Flat Appl) w v) t2)))) (\lambda (H8: (eq T (TSort
+n) (THead (Flat Appl) w v))).(let H9 \def (eq_ind T (TSort n) (\lambda (e:
+T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
+True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
+(THead (Flat Appl) w v) H8) in (False_ind ((eq T (TSort (next g n)) t2) \to
+(ty3 g c0 (THead (Flat Appl) w v) t2)) H9))) c1 (sym_eq C c1 c0 H5) H6 H7))))
+| (tau0_abbr c1 d v0 i H5 w0 H6) \Rightarrow (\lambda (H7: (eq C c1
+c0)).(\lambda (H8: (eq T (TLRef i) (THead (Flat Appl) w v))).(\lambda (H9:
+(eq T (lift (S i) O w0) t2)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef i)
+(THead (Flat Appl) w v)) \to ((eq T (lift (S i) O w0) t2) \to ((getl i c2
(CHead d (Bind Abbr) v0)) \to ((tau0 g d v0 w0) \to (ty3 g c0 (THead (Flat
Appl) w v) t2)))))) (\lambda (H10: (eq T (TLRef i) (THead (Flat Appl) w
v))).(let H11 \def (eq_ind T (TLRef i) (\lambda (e: T).(match e in T return
w v) (THead (Flat Appl) w t3)) (\lambda (x0: T).(\lambda (_: (ty3 g c0 u0
x0)).(ex_ind T (\lambda (t4: T).(ty3 g c0 (THead (Bind Abst) u0 t) t4)) (ty3
g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w t3)) (\lambda (x1:
-T).(\lambda (H18: (ty3 g c0 (THead (Bind Abst) u0 t) x1)).(ex4_3_ind T T T
-(\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind Abst)
-u0 t4) x1)))) (\lambda (_: T).(\lambda (t5: T).(\lambda (_: T).(ty3 g c0 u0
-t5)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0
-(Bind Abst) u0) t t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t6:
-T).(ty3 g (CHead c0 (Bind Abst) u0) t4 t6)))) (ty3 g c0 (THead (Flat Appl) w
-v) (THead (Flat Appl) w t3)) (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4:
-T).(\lambda (_: (pc3 c0 (THead (Bind Abst) u0 x2) x1)).(\lambda (H20: (ty3 g
-c0 u0 x3)).(\lambda (H21: (ty3 g (CHead c0 (Bind Abst) u0) t x2)).(\lambda
-(H22: (ty3 g (CHead c0 (Bind Abst) u0) x2 x4)).(ty3_conv g c0 (THead (Flat
-Appl) w t3) (THead (Flat Appl) w (THead (Bind Abst) u0 x2)) (ty3_appl g c0 w
-u0 H0 t3 x2 (ty3_sconv g c0 t3 x H16 (THead (Bind Abst) u0 t) (THead (Bind
-Abst) u0 x2) (ty3_bind g c0 u0 x3 H20 Abst t x2 H21 x4 H22) H15)) (THead
-(Flat Appl) w v) (THead (Flat Appl) w (THead (Bind Abst) u0 t)) (ty3_appl g
-c0 w u0 H0 v t H2) (pc3_s c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t))
-(THead (Flat Appl) w t3) (pc3_thin_dx c0 t3 (THead (Bind Abst) u0 t) H15 w
-Appl)))))))))) (ty3_gen_bind g Abst c0 u0 t x1 H18)))) (ty3_correct g c0 v
-(THead (Bind Abst) u0 t) H2)))) (ty3_correct g c0 w u0 H0)))) (ty3_correct g
-c0 v t3 H_y))))) t2 H13)) t0 (sym_eq T t0 v H12))) v0 (sym_eq T v0 w H11)))
-H10))) c1 (sym_eq C c1 c0 H6) H7 H8 H5)))) | (tau0_cast c1 v1 v2 H5 t0 t3 H6)
+T).(\lambda (H18: (ty3 g c0 (THead (Bind Abst) u0 t) x1)).(ex3_2_ind T T
+(\lambda (t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind Abst) u0 t4) x1)))
+(\lambda (_: T).(\lambda (t5: T).(ty3 g c0 u0 t5))) (\lambda (t4: T).(\lambda
+(_: T).(ty3 g (CHead c0 (Bind Abst) u0) t t4))) (ty3 g c0 (THead (Flat Appl)
+w v) (THead (Flat Appl) w t3)) (\lambda (x2: T).(\lambda (x3: T).(\lambda (_:
+(pc3 c0 (THead (Bind Abst) u0 x2) x1)).(\lambda (H20: (ty3 g c0 u0
+x3)).(\lambda (H21: (ty3 g (CHead c0 (Bind Abst) u0) t x2)).(ty3_conv g c0
+(THead (Flat Appl) w t3) (THead (Flat Appl) w (THead (Bind Abst) u0 x2))
+(ty3_appl g c0 w u0 H0 t3 x2 (ty3_sconv g c0 t3 x H16 (THead (Bind Abst) u0
+t) (THead (Bind Abst) u0 x2) (ty3_bind g c0 u0 x3 H20 Abst t x2 H21) H15))
+(THead (Flat Appl) w v) (THead (Flat Appl) w (THead (Bind Abst) u0 t))
+(ty3_appl g c0 w u0 H0 v t H2) (pc3_thin_dx c0 (THead (Bind Abst) u0 t) t3
+(ty3_unique g c0 v (THead (Bind Abst) u0 t) H2 t3 H_y) w Appl)))))))
+(ty3_gen_bind g Abst c0 u0 t x1 H18)))) (ty3_correct g c0 v (THead (Bind
+Abst) u0 t) H2)))) (ty3_correct g c0 w u0 H0)))) (ty3_correct g c0 v t3
+H_y))))) t2 H13)) t0 (sym_eq T t0 v H12))) v0 (sym_eq T v0 w H11))) H10))) c1
+(sym_eq C c1 c0 H6) H7 H8 H5)))) | (tau0_cast c1 v1 v2 H5 t0 t3 H6)
\Rightarrow (\lambda (H7: (eq C c1 c0)).(\lambda (H8: (eq T (THead (Flat
Cast) v1 t0) (THead (Flat Appl) w v))).(\lambda (H9: (eq T (THead (Flat Cast)
v2 t3) t2)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead (Flat Cast) v1 t0)
t2) (THead (Flat Cast) v2 t6)) (\lambda (x: T).(\lambda (H18: (ty3 g c0 v2
x)).(ex_ind T (\lambda (t: T).(ty3 g c0 t6 t)) (ty3 g c0 (THead (Flat Cast)
t3 t2) (THead (Flat Cast) v2 t6)) (\lambda (x0: T).(\lambda (H19: (ty3 g c0
-t6 x0)).(ty3_conv g c0 (THead (Flat Cast) v2 t6) v2 (ty3_cast g c0 t6 v2
-(ty3_sconv g c0 t6 x0 H19 t3 v2 H_y0 H17) x H18) (THead (Flat Cast) t3 t2) t3
-(ty3_cast g c0 t2 t3 H0 v2 H_y0) (pc3_s c0 t3 (THead (Flat Cast) v2 t6)
-(pc3_pr2_u c0 t6 (THead (Flat Cast) v2 t6) (pr2_free c0 (THead (Flat Cast) v2
-t6) t6 (pr0_epsilon t6 t6 (pr0_refl t6) v2)) t3 H17))))) (ty3_correct g c0 t2
-t6 H_y)))) (ty3_correct g c0 t3 v2 H_y0))))))) t4 H14)) t5 (sym_eq T t5 t2
-H13))) v1 (sym_eq T v1 t3 H12))) H11))) c1 (sym_eq C c1 c0 H7) H8 H9 H5
-H6))))]) in (H5 (refl_equal C c0) (refl_equal T (THead (Flat Cast) t3 t2))
-(refl_equal T t4))))))))))))) c u t1 H))))).
+t6 x0)).(ty3_conv g c0 (THead (Flat Cast) v2 t6) (THead (Flat Cast) x v2)
+(ty3_cast g c0 t6 v2 (ty3_sconv g c0 t6 x0 H19 t3 v2 H_y0 H17) x H18) (THead
+(Flat Cast) t3 t2) (THead (Flat Cast) v2 t3) (ty3_cast g c0 t2 t3 H0 v2 H_y0)
+(pc3_thin_dx c0 t3 t6 (ty3_unique g c0 t2 t3 H0 t6 H_y) v2 Cast))))
+(ty3_correct g c0 t2 t6 H_y)))) (ty3_correct g c0 t3 v2 H_y0))))))) t4 H14))
+t5 (sym_eq T t5 t2 H13))) v1 (sym_eq T v1 t3 H12))) H11))) c1 (sym_eq C c1 c0
+H7) H8 H9 H5 H6))))]) in (H5 (refl_equal C c0) (refl_equal T (THead (Flat
+Cast) t3 t2)) (refl_equal T t4))))))))))))) c u t1 H))))).
projects / helm.git / blobdiff