[[apply-at-relabeled]] : Correct the misspelled conclusion term. The [[apply-tactic|apply <Conditional> at <Premise>]] 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 apply ... at ... evaluation: hPremise : PremiseType AFTER apply ... at ... evaluation: h<font color="#ff0000">Premise</font> : ConclusionType -- note the term label mismatch with the conclusion type. This confusion is corrected by applying the [[rename'-tactic|rename']] tactic immediately after the apply tactic. **apply hPimpliesQ at hP; rename' (hP : Q) => hQ** With this correction we have relabeled the hypotheses term, hConclusion, to be consistent with its type, ConclusionType: BEFORE apply ... at ... evaluation: hPremise : PremiseType AFTER apply ... at ... evaluation: h<font color="#00b050">Conclusion</font> : ConclusionType --- Author: [[dducoff]] Posted Date: 2026-06-28