+ napply (lt_to_ltb_t ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption]
+ ##| #K'; ngeneralize in match (lt_to_minus … K') in ⊢ ?; #K2;
+ napply (eq_rect_CProp0 ?? (λx.λ_.?) ? ? K2); (* uffa, ancora??? *)
+ nwhd in ⊢ (??? (???????(?%?)?) ?);
+ ngeneralize in match K' in ⊢ ?;
+ napply (nat_rect_CProp0
+ (λx. nindex < x →
+ partition_splits_card_map A P (S n) s f fi
+ (plus (big_op plus_magma_type (minus (minus x nindex) (S O))
+ (λi.λ_.s (S (plus i nindex))) O) nindex2) x = y) ?? n)
+ [ #A; nelim (not_lt_O … A)
+ | #n'; #Hrec; #X; nwhd in ⊢ (???%?);
+ ngeneralize in match
+ (? : ¬ ((plus (big_op plus_magma_type (minus (minus (S n') nindex) (S O))
+ (λi.λ_.s (S (plus i nindex))) O) nindex2) < s (S n'))) in ⊢ ?
+ [ #B1; napply (lt_to_ltb_f ???? B1); #B1'; nwhd in ⊢ (???%?);
+ nrewrite > (minus_S n' nindex …) [##2: napply le_S_S_to_le; nassumption]
+ ngeneralize in match (le_S_S_to_le … X) in ⊢ ?; #X';
+ nelim (le_to_lt_or_eq … X')
+ [##2: #X'';
+ nchange in Hni21 with (nindex2 < s nindex); ngeneralize in match Hni21 in ⊢ ?;
+ nrewrite > X''; nrewrite < (minus_canc n');
+ nrewrite < (minus_canc (S O)); nnormalize in ⊢ (? → %);
+ nelim n'
+ [ #Y; nwhd in ⊢ (??? % ?);
+ ngeneralize in match (minus_lt_to_lt ? (s (S O)) ? Y) in ⊢ ?; #Y';
+ napply (lt_to_ltb_t … Y'); #H; nwhd in ⊢ (???%?);
+
+ nrewrite > (minus_S (minus n' nindex) (S O) …) [##2:
+
+ XXX;
+
+ nelim n in f K' ⊢ ?
+ [ #A; nelim daemon;