(THead (Flat Cast) x v) (ty3_cast g c t v H x H0)))) (ty3_correct g c t v
H)))))).
+theorem ty3_getl_subst0:
+ \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t
+u) \to (\forall (v0: T).(\forall (t0: T).(\forall (i: nat).((subst0 i v0 t
+t0) \to (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c (CHead d
+(Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v w)))))))))))))))
+\def
+ \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (u: T).(\lambda (H:
+(ty3 g c t u)).(ty3_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (_:
+T).(\forall (v0: T).(\forall (t2: T).(\forall (i: nat).((subst0 i v0 t0 t2)
+\to (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d
+(Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v w)))))))))))))) (\lambda
+(c0: C).(\lambda (t2: T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2
+t0)).(\lambda (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i:
+nat).((subst0 i v0 t2 t1) \to (\forall (b: B).(\forall (d: C).(\forall (v:
+T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v
+w))))))))))))).(\lambda (u0: T).(\lambda (t1: T).(\lambda (_: (ty3 g c0 u0
+t1)).(\lambda (H3: ((\forall (v0: T).(\forall (t3: T).(\forall (i:
+nat).((subst0 i v0 u0 t3) \to (\forall (b: B).(\forall (d: C).(\forall (v:
+T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v
+w))))))))))))).(\lambda (_: (pc3 c0 t1 t2)).(\lambda (v0: T).(\lambda (t3:
+T).(\lambda (i: nat).(\lambda (H5: (subst0 i v0 u0 t3)).(\lambda (b:
+B).(\lambda (d: C).(\lambda (v: T).(\lambda (H6: (getl i c0 (CHead d (Bind b)
+v))).(H3 v0 t3 i H5 b d v H6))))))))))))))))))) (\lambda (c0: C).(\lambda (m:
+nat).(\lambda (v0: T).(\lambda (t0: T).(\lambda (i: nat).(\lambda (H0:
+(subst0 i v0 (TSort m) t0)).(\lambda (b: B).(\lambda (d: C).(\lambda (v:
+T).(\lambda (_: (getl i c0 (CHead d (Bind b) v))).(subst0_gen_sort v0 t0 i m
+H0 (ex T (\lambda (w: T).(ty3 g d v w)))))))))))))) (\lambda (n:
+nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: (getl n
+c0 (CHead d (Bind Abbr) u0))).(\lambda (t0: T).(\lambda (H1: (ty3 g d u0
+t0)).(\lambda (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i:
+nat).((subst0 i v0 u0 t1) \to (\forall (b: B).(\forall (d0: C).(\forall (v:
+T).((getl i d (CHead d0 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d0 v
+w))))))))))))).(\lambda (v0: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
+(H3: (subst0 i v0 (TLRef n) t1)).(\lambda (b: B).(\lambda (d0: C).(\lambda
+(v: T).(\lambda (H4: (getl i c0 (CHead d0 (Bind b) v))).(and_ind (eq nat n i)
+(eq T t1 (lift (S n) O v0)) (ex T (\lambda (w: T).(ty3 g d0 v w))) (\lambda
+(H5: (eq nat n i)).(\lambda (_: (eq T t1 (lift (S n) O v0))).(let H7 \def
+(eq_ind_r nat i (\lambda (n0: nat).(getl n0 c0 (CHead d0 (Bind b) v))) H4 n
+H5) in (let H8 \def (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl
+n c0 c1)) H0 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abbr) u0) n
+H0 (CHead d0 (Bind b) v) H7)) in (let H9 \def (f_equal C C (\lambda (e:
+C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
+(CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u0) (CHead d0 (Bind b)
+v) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in
+((let H10 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
+C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k
+in K return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v)
+(getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in
+((let H11 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
+C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t2) \Rightarrow t2]))
+(CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind
+Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in (\lambda (H12: (eq B Abbr
+b)).(\lambda (H13: (eq C d d0)).(let H14 \def (eq_ind_r T v (\lambda (t2:
+T).(getl n c0 (CHead d0 (Bind b) t2))) H8 u0 H11) in (eq_ind T u0 (\lambda
+(t2: T).(ex T (\lambda (w: T).(ty3 g d0 t2 w)))) (let H15 \def (eq_ind_r C d0
+(\lambda (c1: C).(getl n c0 (CHead c1 (Bind b) u0))) H14 d H13) in (eq_ind C
+d (\lambda (c1: C).(ex T (\lambda (w: T).(ty3 g c1 u0 w)))) (let H16 \def
+(eq_ind_r B b (\lambda (b0: B).(getl n c0 (CHead d (Bind b0) u0))) H15 Abbr
+H12) in (ex_intro T (\lambda (w: T).(ty3 g d u0 w)) t0 H1)) d0 H13)) v
+H11))))) H10)) H9)))))) (subst0_gen_lref v0 t1 i n H3))))))))))))))))))
+(\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda
+(H0: (getl n c0 (CHead d (Bind Abst) u0))).(\lambda (t0: T).(\lambda (H1:
+(ty3 g d u0 t0)).(\lambda (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i:
+nat).((subst0 i v0 u0 t1) \to (\forall (b: B).(\forall (d0: C).(\forall (v:
+T).((getl i d (CHead d0 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d0 v
+w))))))))))))).(\lambda (v0: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
+(H3: (subst0 i v0 (TLRef n) t1)).(\lambda (b: B).(\lambda (d0: C).(\lambda
+(v: T).(\lambda (H4: (getl i c0 (CHead d0 (Bind b) v))).(and_ind (eq nat n i)
+(eq T t1 (lift (S n) O v0)) (ex T (\lambda (w: T).(ty3 g d0 v w))) (\lambda
+(H5: (eq nat n i)).(\lambda (_: (eq T t1 (lift (S n) O v0))).(let H7 \def
+(eq_ind_r nat i (\lambda (n0: nat).(getl n0 c0 (CHead d0 (Bind b) v))) H4 n
+H5) in (let H8 \def (eq_ind C (CHead d (Bind Abst) u0) (\lambda (c1: C).(getl
+n c0 c1)) H0 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abst) u0) n
+H0 (CHead d0 (Bind b) v) H7)) in (let H9 \def (f_equal C C (\lambda (e:
+C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
+(CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abst) u0) (CHead d0 (Bind b)
+v) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead d0 (Bind b) v) H7)) in
+((let H10 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
+C).B) with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k
+in K return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
+\Rightarrow Abst])])) (CHead d (Bind Abst) u0) (CHead d0 (Bind b) v)
+(getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead d0 (Bind b) v) H7)) in
+((let H11 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
+C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t2) \Rightarrow t2]))
+(CHead d (Bind Abst) u0) (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind
+Abst) u0) n H0 (CHead d0 (Bind b) v) H7)) in (\lambda (H12: (eq B Abst
+b)).(\lambda (H13: (eq C d d0)).(let H14 \def (eq_ind_r T v (\lambda (t2:
+T).(getl n c0 (CHead d0 (Bind b) t2))) H8 u0 H11) in (eq_ind T u0 (\lambda
+(t2: T).(ex T (\lambda (w: T).(ty3 g d0 t2 w)))) (let H15 \def (eq_ind_r C d0
+(\lambda (c1: C).(getl n c0 (CHead c1 (Bind b) u0))) H14 d H13) in (eq_ind C
+d (\lambda (c1: C).(ex T (\lambda (w: T).(ty3 g c1 u0 w)))) (let H16 \def
+(eq_ind_r B b (\lambda (b0: B).(getl n c0 (CHead d (Bind b0) u0))) H15 Abst
+H12) in (ex_intro T (\lambda (w: T).(ty3 g d u0 w)) t0 H1)) d0 H13)) v
+H11))))) H10)) H9)))))) (subst0_gen_lref v0 t1 i n H3))))))))))))))))))
+(\lambda (c0: C).(\lambda (u0: T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0
+t0)).(\lambda (H1: ((\forall (v0: T).(\forall (t1: T).(\forall (i:
+nat).((subst0 i v0 u0 t1) \to (\forall (b: B).(\forall (d: C).(\forall (v:
+T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v
+w))))))))))))).(\lambda (b: B).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_:
+(ty3 g (CHead c0 (Bind b) u0) t1 t2)).(\lambda (H3: ((\forall (v0:
+T).(\forall (t3: T).(\forall (i: nat).((subst0 i v0 t1 t3) \to (\forall (b0:
+B).(\forall (d: C).(\forall (v: T).((getl i (CHead c0 (Bind b) u0) (CHead d
+(Bind b0) v)) \to (ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda
+(v0: T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H4: (subst0 i v0 (THead
+(Bind b) u0 t1) t3)).(\lambda (b0: B).(\lambda (d: C).(\lambda (v:
+T).(\lambda (H5: (getl i c0 (CHead d (Bind b0) v))).(or3_ind (ex2 T (\lambda
+(u2: T).(eq T t3 (THead (Bind b) u2 t1))) (\lambda (u2: T).(subst0 i v0 u0
+u2))) (ex2 T (\lambda (t4: T).(eq T t3 (THead (Bind b) u0 t4))) (\lambda (t4:
+T).(subst0 (s (Bind b) i) v0 t1 t4))) (ex3_2 T T (\lambda (u2: T).(\lambda
+(t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2: T).(\lambda (_:
+T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4: T).(subst0 (s (Bind b)
+i) v0 t1 t4)))) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (H6: (ex2 T
+(\lambda (u2: T).(eq T t3 (THead (Bind b) u2 t1))) (\lambda (u2: T).(subst0 i
+v0 u0 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t3 (THead (Bind b) u2 t1)))
+(\lambda (u2: T).(subst0 i v0 u0 u2)) (ex T (\lambda (w: T).(ty3 g d v w)))
+(\lambda (x: T).(\lambda (_: (eq T t3 (THead (Bind b) x t1))).(\lambda (H8:
+(subst0 i v0 u0 x)).(H1 v0 x i H8 b0 d v H5)))) H6)) (\lambda (H6: (ex2 T
+(\lambda (t4: T).(eq T t3 (THead (Bind b) u0 t4))) (\lambda (t4: T).(subst0
+(s (Bind b) i) v0 t1 t4)))).(ex2_ind T (\lambda (t4: T).(eq T t3 (THead (Bind
+b) u0 t4))) (\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4)) (ex T (\lambda
+(w: T).(ty3 g d v w))) (\lambda (x: T).(\lambda (_: (eq T t3 (THead (Bind b)
+u0 x))).(\lambda (H8: (subst0 (s (Bind b) i) v0 t1 x)).(H3 v0 x (S i) H8 b0 d
+v (getl_head (Bind b) i c0 (CHead d (Bind b0) v) H5 u0))))) H6)) (\lambda
+(H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2
+t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_:
+T).(\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4))))).(ex3_2_ind T T
+(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda
+(u2: T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4:
+T).(subst0 (s (Bind b) i) v0 t1 t4))) (ex T (\lambda (w: T).(ty3 g d v w)))
+(\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (eq T t3 (THead (Bind b) x0
+x1))).(\lambda (H8: (subst0 i v0 u0 x0)).(\lambda (_: (subst0 (s (Bind b) i)
+v0 t1 x1)).(H1 v0 x0 i H8 b0 d v H5)))))) H6)) (subst0_gen_head (Bind b) v0
+u0 t1 t3 i H4)))))))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda
+(u0: T).(\lambda (_: (ty3 g c0 w u0)).(\lambda (H1: ((\forall (v0:
+T).(\forall (t0: T).(\forall (i: nat).((subst0 i v0 w t0) \to (\forall (b:
+B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b) v)) \to (ex
+T (\lambda (w0: T).(ty3 g d v w0))))))))))))).(\lambda (v: T).(\lambda (t0:
+T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u0 t0))).(\lambda (H3:
+((\forall (v0: T).(\forall (t1: T).(\forall (i: nat).((subst0 i v0 v t1) \to
+(\forall (b: B).(\forall (d: C).(\forall (v1: T).((getl i c0 (CHead d (Bind
+b) v1)) \to (ex T (\lambda (w0: T).(ty3 g d v1 w0))))))))))))).(\lambda (v0:
+T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (H4: (subst0 i v0 (THead (Flat
+Appl) w v) t1)).(\lambda (b: B).(\lambda (d: C).(\lambda (v1: T).(\lambda
+(H5: (getl i c0 (CHead d (Bind b) v1))).(or3_ind (ex2 T (\lambda (u2: T).(eq
+T t1 (THead (Flat Appl) u2 v))) (\lambda (u2: T).(subst0 i v0 w u2))) (ex2 T
+(\lambda (t2: T).(eq T t1 (THead (Flat Appl) w t2))) (\lambda (t2: T).(subst0
+(s (Flat Appl) i) v0 v t2))) (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq
+T t1 (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i
+v0 w u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v
+t2)))) (ex T (\lambda (w0: T).(ty3 g d v1 w0))) (\lambda (H6: (ex2 T (\lambda
+(u2: T).(eq T t1 (THead (Flat Appl) u2 v))) (\lambda (u2: T).(subst0 i v0 w
+u2)))).(ex2_ind T (\lambda (u2: T).(eq T t1 (THead (Flat Appl) u2 v)))
+(\lambda (u2: T).(subst0 i v0 w u2)) (ex T (\lambda (w0: T).(ty3 g d v1 w0)))
+(\lambda (x: T).(\lambda (_: (eq T t1 (THead (Flat Appl) x v))).(\lambda (H8:
+(subst0 i v0 w x)).(H1 v0 x i H8 b d v1 H5)))) H6)) (\lambda (H6: (ex2 T
+(\lambda (t2: T).(eq T t1 (THead (Flat Appl) w t2))) (\lambda (t2: T).(subst0
+(s (Flat Appl) i) v0 v t2)))).(ex2_ind T (\lambda (t2: T).(eq T t1 (THead
+(Flat Appl) w t2))) (\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2)) (ex
+T (\lambda (w0: T).(ty3 g d v1 w0))) (\lambda (x: T).(\lambda (_: (eq T t1
+(THead (Flat Appl) w x))).(\lambda (H8: (subst0 (s (Flat Appl) i) v0 v
+x)).(H3 v0 x (s (Flat Appl) i) H8 b d v1 H5)))) H6)) (\lambda (H6: (ex3_2 T T
+(\lambda (u2: T).(\lambda (t2: T).(eq T t1 (THead (Flat Appl) u2 t2))))
+(\lambda (u2: T).(\lambda (_: T).(subst0 i v0 w u2))) (\lambda (_:
+T).(\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2))))).(ex3_2_ind T T
+(\lambda (u2: T).(\lambda (t2: T).(eq T t1 (THead (Flat Appl) u2 t2))))
+(\lambda (u2: T).(\lambda (_: T).(subst0 i v0 w u2))) (\lambda (_:
+T).(\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2))) (ex T (\lambda (w0:
+T).(ty3 g d v1 w0))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (eq T t1
+(THead (Flat Appl) x0 x1))).(\lambda (_: (subst0 i v0 w x0)).(\lambda (H9:
+(subst0 (s (Flat Appl) i) v0 v x1)).(H3 v0 x1 (s (Flat Appl) i) H9 b d v1
+H5)))))) H6)) (subst0_gen_head (Flat Appl) v0 w v t1 i H4)))))))))))))))))))
+(\lambda (c0: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1
+t2)).(\lambda (H1: ((\forall (v0: T).(\forall (t0: T).(\forall (i:
+nat).((subst0 i v0 t1 t0) \to (\forall (b: B).(\forall (d: C).(\forall (v:
+T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v
+w))))))))))))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda (H3:
+((\forall (v0: T).(\forall (t3: T).(\forall (i: nat).((subst0 i v0 t2 t3) \to
+(\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b)
+v)) \to (ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda (v0:
+T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H4: (subst0 i v0 (THead (Flat
+Cast) t2 t1) t3)).(\lambda (b: B).(\lambda (d: C).(\lambda (v: T).(\lambda
+(H5: (getl i c0 (CHead d (Bind b) v))).(or3_ind (ex2 T (\lambda (u2: T).(eq T
+t3 (THead (Flat Cast) u2 t1))) (\lambda (u2: T).(subst0 i v0 t2 u2))) (ex2 T
+(\lambda (t4: T).(eq T t3 (THead (Flat Cast) t2 t4))) (\lambda (t4:
+T).(subst0 (s (Flat Cast) i) v0 t1 t4))) (ex3_2 T T (\lambda (u2: T).(\lambda
+(t4: T).(eq T t3 (THead (Flat Cast) u2 t4)))) (\lambda (u2: T).(\lambda (_:
+T).(subst0 i v0 t2 u2))) (\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat
+Cast) i) v0 t1 t4)))) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (H6:
+(ex2 T (\lambda (u2: T).(eq T t3 (THead (Flat Cast) u2 t1))) (\lambda (u2:
+T).(subst0 i v0 t2 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t3 (THead (Flat
+Cast) u2 t1))) (\lambda (u2: T).(subst0 i v0 t2 u2)) (ex T (\lambda (w:
+T).(ty3 g d v w))) (\lambda (x: T).(\lambda (_: (eq T t3 (THead (Flat Cast) x
+t1))).(\lambda (H8: (subst0 i v0 t2 x)).(H3 v0 x i H8 b d v H5)))) H6))
+(\lambda (H6: (ex2 T (\lambda (t4: T).(eq T t3 (THead (Flat Cast) t2 t4)))
+(\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1 t4)))).(ex2_ind T (\lambda
+(t4: T).(eq T t3 (THead (Flat Cast) t2 t4))) (\lambda (t4: T).(subst0 (s
+(Flat Cast) i) v0 t1 t4)) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (x:
+T).(\lambda (_: (eq T t3 (THead (Flat Cast) t2 x))).(\lambda (H8: (subst0 (s
+(Flat Cast) i) v0 t1 x)).(H1 v0 x (s (Flat Cast) i) H8 b d v H5)))) H6))
+(\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
+(Flat Cast) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 t2 u2)))
+(\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1
+t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
+(Flat Cast) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 t2 u2)))
+(\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1 t4))) (ex T
+(\lambda (w: T).(ty3 g d v w))) (\lambda (x0: T).(\lambda (x1: T).(\lambda
+(_: (eq T t3 (THead (Flat Cast) x0 x1))).(\lambda (H8: (subst0 i v0 t2
+x0)).(\lambda (_: (subst0 (s (Flat Cast) i) v0 t1 x1)).(H3 v0 x0 i H8 b d v
+H5)))))) H6)) (subst0_gen_head (Flat Cast) v0 t2 t1 t3 i H4))))))))))))))))))
+c t u H))))).
+
projects / helm.git / blobdiff