Swap bound variable tactic #
This files defines a tactic swap_var
whose main purpose is to be a weaker
version of wlog
that juggles bound names.
It is a helper around the core tactic rename
.
swap_var old new
renames all names namedold
tonew
and vice versa in the goal and all hypotheses.
example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
begin
split,
work_on_goal 1 { swap_var [P Q] },
all_goals { exact ‹P› }
end