Remove `bi.tactics`

The file bi.tactics contains mostly legacy stuff that predates the proof mode, and has bitrot quite a bit since then (see #373 (closed)).

Some tactics in this file are used to bootstrap the proof mode, but this MR shows that all of these proofs can be replaced by one-liner manual proofs.

@lepigre noticed that something akin to sep_solve_entails could be useful in clients of Iris. Maybe we should have some tactic for that in the proofmode? For example:

Ltac iSolveSepEntails :=
  iIntros;
  repeat iMatchHyp (fun H P =>
    lazymatch P with
    | (_ ∗ _)%I => iDestruct H as "[??]"
    | (∃ _, _)%I => iDestruct H as (?) "?"
    end);
  eauto with iFrame.

Lemma test2 {PROP : bi} (P Q R : PROP) (Φ Ψ : nat → PROP) :
  P ∗ R ∗ Q ∗ P ∗ R ∗ (∃ x, Φ x ∗ Ψ x) ∗ Q ∗ P ∗ R ∗ Q
  ⊢ ∃ y, Ψ y ∗ (R ∗ Q ∗ P) ∗ R ∗ (∃ x, Q ∗ Φ x) ∗ P ∗ (R ∗ Q ∗ P).
Proof. iSolveSepEntails. Qed.