[ cases l1; simplify; [intros; destruct H | unfold Not; intros; destruct H1;]
| intros 3 (tl1 IH l2); cases l2;
[ unfold Not; intros; destruct H1;
| simplify; intros;
cases (b2pT ? ? (andbPF ? ?) (p2bT ? ? (negbP ?) H)); clear H;
[ cases l1; simplify; [intros; destruct H | unfold Not; intros; destruct H1;]
| intros 3 (tl1 IH l2); cases l2;
[ unfold Not; intros; destruct H1;
| simplify; intros;
cases (b2pT ? ? (andbPF ? ?) (p2bT ? ? (negbP ?) H)); clear H;