include "nf2/lift1.ma".
+include "csuba/arity.ma".
+
include "arity/lift1.ma".
include "arity/aprem.ma".
include "llt/props.ma".
+include "drop1/getl.ma".
+
include "drop1/props.ma".
+include "lift1/props.ma".
+
theorem sc3_arity_gen:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((sc3 g a c
t) \to (arity g c t a)))))
(THeads (Flat Appl) vs (TLRef i)))))))))) (arity_appls_abbr g c d v i H2 vs
(AHead a0 a1) H4) (\lambda (d0: C).(\lambda (w: T).(\lambda (H6: (sc3 g a0 d0
w)).(\lambda (is: PList).(\lambda (H7: (drop1 is d0 c)).(let H_x \def
-(drop1_getl_trans is c d0 H7 Abbr d v i H2) in (let H8 \def H_x in (ex_ind C
-(\lambda (e2: C).(getl (trans is i) d0 (CHead e2 (Bind Abbr) (ctrans is i
-v)))) (sc3 g a1 d0 (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs
-(TLRef i))))) (\lambda (x: C).(\lambda (H9: (getl (trans is i) d0 (CHead x
-(Bind Abbr) (ctrans is i v)))).(let H_y \def (H0 (TCons w (lifts1 is vs))) in
-(eq_ind_r T (THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))) (\lambda
-(t: T).(sc3 g a1 d0 (THead (Flat Appl) w t))) (eq_ind_r T (TLRef (trans is
-i)) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w (THeads (Flat Appl)
-(lifts1 is vs) t)))) (H_y (trans is i) x (ctrans is i v) d0 (eq_ind T (lift1
-is (lift (S i) O v)) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w
-(THeads (Flat Appl) (lifts1 is vs) t)))) (eq_ind T (lift1 is (THeads (Flat
-Appl) vs (lift (S i) O v))) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w
-t))) (H5 d0 w H6 is H7) (THeads (Flat Appl) (lifts1 is vs) (lift1 is (lift (S
-i) O v))) (lifts1_flat Appl is (lift (S i) O v) vs)) (lift (S (trans is i)) O
-(ctrans is i v)) (lift1_free is i v)) H9) (lift1 is (TLRef i)) (lift1_lref is
-i)) (lift1 is (THeads (Flat Appl) vs (TLRef i))) (lifts1_flat Appl is (TLRef
-i) vs))))) H8))))))))))) H3))))))))))))) a)).
+(drop1_getl_trans is c d0 H7 Abbr d v i H2) in (let H8 \def H_x in (ex2_ind C
+(\lambda (e2: C).(drop1 (ptrans is i) e2 d)) (\lambda (e2: C).(getl (trans is
+i) d0 (CHead e2 (Bind Abbr) (lift1 (ptrans is i) v)))) (sc3 g a1 d0 (THead
+(Flat Appl) w (lift1 is (THeads (Flat Appl) vs (TLRef i))))) (\lambda (x:
+C).(\lambda (_: (drop1 (ptrans is i) x d)).(\lambda (H10: (getl (trans is i)
+d0 (CHead x (Bind Abbr) (lift1 (ptrans is i) v)))).(let H_y \def (H0 (TCons w
+(lifts1 is vs))) in (eq_ind_r T (THeads (Flat Appl) (lifts1 is vs) (lift1 is
+(TLRef i))) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w t))) (eq_ind_r
+T (TLRef (trans is i)) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w
+(THeads (Flat Appl) (lifts1 is vs) t)))) (H_y (trans is i) x (lift1 (ptrans
+is i) v) d0 (eq_ind T (lift1 is (lift (S i) O v)) (\lambda (t: T).(sc3 g a1
+d0 (THead (Flat Appl) w (THeads (Flat Appl) (lifts1 is vs) t)))) (eq_ind T
+(lift1 is (THeads (Flat Appl) vs (lift (S i) O v))) (\lambda (t: T).(sc3 g a1
+d0 (THead (Flat Appl) w t))) (H5 d0 w H6 is H7) (THeads (Flat Appl) (lifts1
+is vs) (lift1 is (lift (S i) O v))) (lifts1_flat Appl is (lift (S i) O v)
+vs)) (lift (S (trans is i)) O (lift1 (ptrans is i) v)) (lift1_free is i v))
+H10) (lift1 is (TLRef i)) (lift1_lref is i)) (lift1 is (THeads (Flat Appl) vs
+(TLRef i))) (lifts1_flat Appl is (TLRef i) vs)))))) H8)))))))))))
+H3))))))))))))) a)).
theorem sc3_cast:
\forall (g: G).(\forall (a: A).(\forall (vs: TList).(\forall (c: C).(\forall