. obtain ⟨_, e⟩ := hTc; subst_vars; dsimp [Axioms.Tc, TrivTranslation, toPropFormula]; apply imp_id!;
case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hTc : p✝ ∈ 𝗧𝗰
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
no goals