- [#H1 @(absurd … (\P H1)) % #Hfalse
- cut (∀A,P,a,a1,h,h1.mk_Sig A P a h = mk_Sig A P a1 h1 → a = a1)
- [#A #P #a #a1 #h #h1 #H destruct (H) %] #Hcut
- lapply (Hcut nat (λi.i<m) i n ? ? Hfalse) #Hfalse @(absurd … ltni)
- @le_to_not_lt >Hfalse @le_n
- |<(notb_notb (memb …)) >Hind normalize /2/
+ [whd in ⊢ (??%?→?); #H1 @(absurd … ltni) @le_to_not_lt
+ >(eqb_true_to_eq … H1) @le_n
+ |<(notb_notb (memb …)) >Hind normalize /2 by lt_to_le, absurd/