intros (d e l s); elim l (hd tl IH); [cases s;simplify;[2: rewrite > andbC] reflexivity]
simplify; rewrite > IH; cases s; simplify; [reflexivity]
unfold list_eqType; simplify;
intros (d e l s); elim l (hd tl IH); [cases s;simplify;[2: rewrite > andbC] reflexivity]
simplify; rewrite > IH; cases s; simplify; [reflexivity]
unfold list_eqType; simplify;
intros (d s l x); elim s; [cases x] simplify; try reflexivity; rewrite > mem_concat;
rewrite > H; clear H; rewrite > mem_multes; cases x; simplify; [reflexivity]
unfold list_eqType; simplify; apply (cmpP ? t s1); intros (E);
intros (d s l x); elim s; [cases x] simplify; try reflexivity; rewrite > mem_concat;
rewrite > H; clear H; rewrite > mem_multes; cases x; simplify; [reflexivity]
unfold list_eqType; simplify; apply (cmpP ? t s1); intros (E);