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;