+ ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2;
+ ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ?
+ [##2: napply (. #‡(†?));##[##3: napply Hni2 |##2: ##skip | nassumption]##]
+ *; #nindex2; *; #Hni21; #Hni22;
+ napply (ex_intro … (plus (big_plus nindex (λi.λ_.s i)) nindex2)); napply conj
+ [ nwhd in Hni1; nelim daemon
+ | nwhd in ⊢ (???%?);
+ (* BEL POSTO DOVE FARE UN LEMMA *)
+ (* invariante: Hni1; altre premesse: Hni1, Hni22 *)
+ nchange in Hni1 with (nindex < n); ngeneralize in match Hni1 in ⊢ ?;
+ nelim n
+ [ #A (* decompose *)
+ | #index'; #Hrec;
+ ]
+ ]