napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
*; #nindex2; *; #Hni21; #Hni22;
nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);
napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
*; #nindex2; *; #Hni21; #Hni22;
nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);