(lift1 is t0))))))))).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H4:
(drop1 is d1 c)).(\lambda (c2: C).(\lambda (H5: (csubc g d1 c2)).(let H_y
\def (H1 d1 is H4 c2 H5) in (let H_y0 \def (H3 d1 is H4 c2 H5) in (let H6
-\def H_y0 in (and_ind (arity g c2 (lift1 is t0) (AHead a1 a2)) (\forall (d:
+\def H_y0 in (land_ind (arity g c2 (lift1 is t0) (AHead a1 a2)) (\forall (d:
C).(\forall (w: T).((sc3 g a1 d w) \to (\forall (is0: PList).((drop1 is0 d
c2) \to (sc3 g a2 d (THead (Flat Appl) w (lift1 is0 (lift1 is t0)))))))))
(sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0))) (\lambda (_: (arity g c2