- #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; *)
- (* napplyS start non va *)
- ncut (S (length T L) = ((length T L)+0+1)); ##[//##] #Heq;
- ncheck start.
- napplyS start;/2/;