-(*
- napplyS (app (substl D N@G1) (subst P (length T D) N) A (subst R (length T D) N) (subst S (length T D) N) ?).
- *)
- nlapply (subst_lemma R S N (length ? D) 0); #sl;
- nrewrite < (plus_n_O ?) in sl; #sl;
- nrewrite > sl;
- napply app; nnormalize in Hind1;/2/;