reflexivity;
| cases (H (b2pT ? ? (eqP d s t) Hcmp))
]
-| constructor 2; unfold Not; intros (H);
- (* XXX destruct H; *)
- change in Hcmp with (cmp d (match {?,ps} with [(mk_sigma s _)⇒s]) t = false);
- rewrite > H in Hcmp; simplify in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;
-]
+| constructor 2; unfold Not; intros (H); destruct H;
+ rewrite > Hcut in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;]
qed.
definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p).
generalize in match (ocmp ? a b) in ⊢ (? ? ? % → %); intros 1 (c);
cases c; intros (H); [ apply reflect_true | apply reflect_false ];
generalize in match H; clear H;
-cases a; cases b;
-[1: intros; reflexivity;
-|2,3: intros (H); destruct H;
-|4: intros (H); simplify in H; rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity;
- (* se faccio la rewrite diretta non tipa *)
-|5: intros (H H1); destruct H
-|6,7: unfold Not; intros (H H1); destruct H1
-|8: unfold Not; simplify; intros (H 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;
-] qed.
+cases a; cases b; simplify; intros (H);
+[1: reflexivity;
+|2,3,5: destruct H;
+|4: rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity;
+|6,7: unfold Not; intros (H1); destruct H1
+|8: unfold Not; intros (H1); destruct H1;
+ rewrite > Hcut in H; rewrite > cmp_refl in H; destruct H;]
+qed.
definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d).
definition option_canonical_eqType : ∀d:eqType.d → option_eqType d ≝