Apply at #
A tactic for applying functions at hypotheses.
apply t at i will use forward reasoning with t at the hypothesis i.
Explicitly, if t : α₁ → ⋯ → αᵢ → ⋯ → αₙ and i has type αᵢ, then this tactic will add
metavariables/goals for any terms of αⱼ for j = 1, …, i-1,
then replace the type of i with αᵢ₊₁ → ⋯ → αₙ by applying those metavariables and the
original i.
Equations
- One or more equations did not get rendered due to their size.