Ltac pointlessRecurse depth hyp cont list :=
  match depth with
    | 0 => (specialize (hyp list); cont) || fail 100 "Ran out of depth"
    | S ?n => (specialize (hyp list); cont) || pointlessRecurse n hyp cont (true :: list) || pointlessRecurse n hyp cont (false :: list)
    | _ => fail 100 "recursion failed"
  end.

Ltac pointlessSearch depth :=
  match goal with
    | [ H : forall ls1 ls2, _ |- _ ] => pointlessRecurse depth H ltac:(pointlessSearch depth) (@nil bool)
    | [ H : forall ls, _ |- _ ] => pointlessRecurse depth H discriminate (@nil bool)
    | _ => fail 1 "fail on hyp"
  end.

Ltac pointless depth :=
  match goal with
    | [ H : _ |- _ ] => fail 1 "Should be first tactic run"
    | [ |- ?P ] => assert (Hcontr : P -> False); [ intro Hn; specialize (Hn bool); pointlessSearch depth | ]
    | _ => fail 1 "failed"
  end.