| simplify; intros;
cases (b2pT ? ? (andbPF ? ?) (p2bT ? ? (negbP ?) H)); clear H;
[ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1;
- destruct H; rewrite > Hcut in H'; apply H'; reflexivity;
+ destruct H; apply H'; reflexivity;
| intros; lapply (IH ? H1) as H'; destruct H;
- rewrite > Hcut1 in H'; apply H'; reflexivity;]]]]
+ apply H'; reflexivity;]]]]
qed.
definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).