\forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (u:
T).((ty3 g c (THead (Bind Abst) v t) u) \to ((pc3 c u v) \to (\forall (P:
Prop).P)))))))
\forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (u:
T).((ty3 g c (THead (Bind Abst) v t) u) \to ((pc3 c u v) \to (\forall (P:
Prop).P)))))))
in (leq_ahead_asucc_false g x2 (asucc g x3) (arity_mono g c v (asucc g (AHead
x2 x3)) H12 (asucc g x2) H10) P))))))) H8))))) H5))))))))) (ty3_gen_bind g
Abst c v t u H1)))))))))).
in (leq_ahead_asucc_false g x2 (asucc g x3) (arity_mono g c v (asucc g (AHead
x2 x3)) H12 (asucc g x2) H10) P))))))) H8))))) H5))))))))) (ty3_gen_bind g
Abst c v t u H1)))))))))).
(S O) O H8 c (drop_drop (Bind Abst) O c c (drop_refl c) w)) (asucc g x2)
H11)) P)))) H9)))))) H6))))))) H3)))) (ty3_correct g (CHead c (Bind Abst) w)
t (lift (S O) O u2) H0))))))))))).
(S O) O H8 c (drop_drop (Bind Abst) O c c (drop_refl c) w)) (asucc g x2)
H11)) P)))) H9)))))) H6))))))) H3)))) (ty3_correct g (CHead c (Bind Abst) w)
t (lift (S O) O u2) H0))))))))))).
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t
u) \to ((pc3 c u t) \to (\forall (P: Prop).P))))))
\def
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t
u) \to ((pc3 c u t) \to (\forall (P: Prop).P))))))
\def
(a1: A).(arity g c t (asucc g a1))) P (\lambda (x: A).(\lambda (H2: (arity g
c t x)).(\lambda (H3: (arity g c t (asucc g x))).(leq_asucc_false g x
(arity_mono g c t (asucc g x) H3 x H2) P)))) H1)))))))))).
(a1: A).(arity g c t (asucc g a1))) P (\lambda (x: A).(\lambda (H2: (arity g
c t x)).(\lambda (H3: (arity g c t (asucc g x))).(leq_asucc_false g x
(arity_mono g c t (asucc g x) H3 x H2) P)))) H1)))))))))).
(asucc g a1))) (sn3 c t) (\lambda (x: A).(\lambda (H1: (arity g c t
x)).(\lambda (_: (arity g c u (asucc g x))).(sc3_sn3 g x c t (sc3_arity g c t
x H1))))) H0))))))).
(asucc g a1))) (sn3 c t) (\lambda (x: A).(\lambda (H1: (arity g c t
x)).(\lambda (_: (arity g c u (asucc g x))).(sc3_sn3 g x c t (sc3_arity g c t
x H1))))) H0))))))).