(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/list_aux/".
-
include "list/list.ma".
include "decidable_kit/eqtype.ma".
include "nat/plus.ma".
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).