have d₁ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ p := conj₂'! deducible_iff_trivTranslation
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
d₁ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ p
⊢ 𝐓𝐫𝐢𝐯 ⊢! p