+ #tjN1; nnormalize; ndestruct;
+ ncheck( let clause_829:
+ ∀x1947: ?.
+ ∀x1948: ?.
+ ∀x1949: ?.
+ ∀x1950: ?.
+ ∀x1951: ?.
+ eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951)
+ (subst (lift x1947 x1949 x1951) (plus x1948 (plus x1949 x1951))
+ x1950)
+ ≝ λx1947:?.
+ λx1948:?.
+ λx1949:?.
+ λx1950:?.
+ λx1951:?.
+ rewrite_l nat (plus (plus x1948 x1949) x1951)
+ (λx:nat.
+ eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951)
+ (subst (lift x1947 x1949 x1951) x x1950))
+ (lift_subst_ijk x1950 x1947 x1951 x1948 x1949)
+ (plus x1948 (plus x1949 x1951))
+ (associative_plus x1948 x1949 x1951) in
+ let clause_60: ∀x156: ?. eq nat (S x156) (plus x156 (S O))
+ ≝ λx156:?.
+ rewrite_r nat (plus x156 O) (λx:nat. eq nat (S x) (plus x156 (S O)))
+ (plus_n_Sm x156 O) x156 (plus_n_O x156) in
+ let clause_996 :
+ eq Type
+ (TJ (cons T (subst ? ? ?) ?) (Rel O)
+ (subst (lift ? O (S O)) (plus ? (S O)) ?))
+ (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))
+ ≝ rewrite_l nat (S (length T L))
+ (λx:nat.
+ eq Type
+ (TJ
+ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) x N1))
+ (TJ
+ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
+ (refl Type
+ (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
+ (plus (length T L) (S O)) (clause_60 (length T L)) in
+ let clause_995:
+ eq Type
+ (TJ (cons T (subst ? ? ?) ?) (Rel O)
+ (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?))
+ (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))
+ ≝ rewrite_l nat (S O)
+ (λx:nat.
+ eq Type
+ (TJ (cons T (subst ? ? ?) ?) (Rel O)
+ (subst (lift ? O (S O)) (plus ? x) ?))
+ (TJ
+ (cons T (subst H (length T L) N1)
+ (append T (substl L N1) G1)) (Rel O)
+ (subst (lift H O (S O)) (S (length T L)) N1))) clause_996
+ (plus O (S O)) (plus_O_n (S O)) in
+ rewrite_r T
+ (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?)
+ (λx:T.
+ eq Type
+ (TJ (cons T (subst ? (plus ? O) ?) ?) (Rel O) x)
+ (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
+ (rewrite_l nat ?
+ (λx:nat.
+ eq Type
+ (TJ (cons T (subst ? x ?) ?) (Rel O)
+ (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?))
+ (TJ
+ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
+ clause_995 (plus ? O) (plus_n_O ?))
+ (lift (subst ? (plus ? O) ?) O (S O))
+ (clause_829 ? ? O ? (S O))
+).
+ napplyS start;
+ (* napplyS start; *)