(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/list_aux/".
-
include "list/list.ma".
include "decidable_kit/eqtype.ma".
include "nat/plus.ma".
apply (list_ind2 ? ? ? ? ? Hl); [1: intros; reflexivity]
simplify; intros (tl1 tl2 hd1 hd2 IH H); cases (b2pT ? ? (andbP ? ?) H);
rewrite > (IH H2); rewrite > (b2pT ? ? (eqP d ? ?) H1); reflexivity
-| generalize in match H; clear H; generalize in match l2; clear l2;
- elim l1 1 (l1 x1);
+| elim l1 in H l2 ⊢ % 1 (l1 x1);
[ cases l1; simplify; [intros; destruct H | unfold Not; intros; destruct H1;]
| intros 3 (tl1 IH l2); cases l2;
[ unfold Not; intros; destruct H1;
apply H'; reflexivity;]]]]
qed.
-definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).
\ No newline at end of file
+definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).