-|8: unfold Not; intros (H1);
- (* ancora injection non va *)
- cut (s = s1); [ rewrite > Hcut in H; rewrite > cmp_refl in H; destruct H;].
- change with (match (Some d s) with
- [ None ⇒ s | (Some s) ⇒ s] = s1); rewrite > H1;
- simplify; reflexivity;]
+|8: unfold Not; intros (H1); destruct H1;
+ rewrite > Hcut in H; rewrite > cmp_refl in H; destruct H;]