. intro h;
  have d₁ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ p := conj₂'! deducible_iff_trivTranslation;
  have d₂ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ := by simpa only [TrivTranslation.back] using of_classical h;
  exact d₁ ⨀ d₂;
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pᵀᴾ) ⋯ → 𝐓𝐫𝐢𝐯 ⊢! p
no goals