(* S d = S d → ? e' in realta' eq nat (S d) (S d) ... *)
ncases l in ⊢ (? ? % ? → %);
##[ ##1: #dsc; #H; nelim (nat_destruct_0_S … H)
(* S d = S d → ? e' in realta' eq nat (S d) (S d) ... *)
ncases l in ⊢ (? ? % ? → %);
##[ ##1: #dsc; #H; nelim (nat_destruct_0_S … H)