should `clear_` tactic also clear inaccessible hypotheses?

In mathlib3, pairwise_and_iff has a usage of clear_ with this context:

α : Type u_1,
R S : α → α → Prop,
l : list α,
_x : pairwise R l ∧ pairwise S l,
_fun_match : pairwise R l ∧ pairwise S l → pairwise (λ (a b : α), R a b ∧ S a b) l,
hR : pairwise R l,
hS : pairwise S l
⊢ pairwise (λ (a b : α), R a b ∧ S a b) l

(see https://github.com/leanprover-community/mathlib/blob/aff61c0f687c5d366edb248791f26fa69a4adfe2/src/data/list/pairwise.lean#L67)

A direct translation into Lean 4 leads to this context in the same place:

α : Type u_1
R : α → α → Prop
a : α
l : List α
S : α → α → Prop
: Pairwise R l ∧ Pairwise S l
hR : Pairwise R l
hS : Pairwise S l
⊢ Pairwise (fun a b => R a b ∧ S a b) l

In this case, the current version of mathlib4's clear_ won't drop the Pairwise R l ∧ Pairwise S l hypothesis, because it is anonymous inaccessible. We need to drop that hypothesis to get the later induction to work. It's easy enough to work around this problem by adapting the proof a bit, but it would be nice if we could have a direct translation. What would make most sense to me is for mathlib4's clear_ to also drop unnamed hypotheses (in addition to hypotheses whose names start with _). We could even make the behavior configurable.

Start with the clear_ tactic behavior and the pairwise_and_iff usage in src/data/list/pairwise.lean around line 67. Reproduce the Lean 4 context shown in the issue, then determine how inaccessible hypotheses should be handled and verify that the translated induction proceeds after the hypothesis is removed.