induction p using Formula.rec' with
| hbox =>
  apply iff_intro!;
  . exact imply₁'! verum!
  . exact dhyp! (by simp)
| himp _ _ ih₁ ih₂ => exact imp_replace_iff! ih₁ ih₂;
| hand _ _ ih₁ ih₂ => exact and_replace_iff! ih₁ ih₂;
| hor _ _ ih₁ ih₂ => exact or_replace_iff! ih₁ ih₂;
| _ => apply iff_id!
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p ⟷ pⱽ
no goals