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
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