Rule. bij_elimr
(H ⊢ A ↔ B) → (H ⊢ B → A)