induction p using Formula.rec' with
| hbox p ih =>
  simp [TrivTranslation];
  apply iff_intro!;
  . exact imp_trans! axiomT! (conj₁'! ih)
  . exact imp_trans! (conj₂'! ih) axiomTc!
| 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