[1: generalize in match H; rewrite > (b2pT ? ? (eqP (list_eqType d2) ? ?) H2);
intros; clear H H2; rewrite < (pirrel ? ? ? H1 H3 (eqType_decidable nat_eqType));
reflexivity
[1: generalize in match H; rewrite > (b2pT ? ? (eqP (list_eqType d2) ? ?) H2);
intros; clear H H2; rewrite < (pirrel ? ? ? H1 H3 (eqType_decidable nat_eqType));
reflexivity
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);