[[apply-at-relabeled]] : Correct the misspelled conclusion term. The [[apply-at-tactic]] tactic applies modus ponens, but, unfortunately, it misspells the conclusion term. That is, the label of the premise term is unchanged when it's type changes to the conclusion type: BEFORE the tactic application, the premise term correctly labels a witness of the premise type: hPremise : PremiseType APPLY the tactic: `apply hPimpliesQ at hP` AFTER the tactic application, the premise term incorrectly labels a witness of the conclusion type: h<font color="#ff0000">Premise</font> : ConclusionType This confusion is corrected by applying the [[rename'-tactic|rename']] tactic immediately after the apply tactic, which corrects the spelling of the conclusion term, as in: apply hPimpliesQ at hP; rename' (hP : Q) => hQ So, now the conclusion term has a corrected spelling, as in: BEFORE the tactic application, the premise term correctly labels a witness of the premise type: hPremise : PremiseType APPLY the modified tactic: **apply hPimpliesQ at hP; rename' (hP : Q) => hQ** AFTER the tactic application, the conclusion term changes from h<font color="#ff0000">Premise</font> to the corrected label, h<font color="#00b050">Conclusion</font>: h<font color="#00b050">Conclusion</font> : ConclusionType --- Author: [[dducoff]] Posted Date: 2026-06-28