bind free variable for decide

Stream: new members

[Simon Daniel]

hello,
If i have a free Variable, that is bound to a value by a proposition, the decide tactic fails. Is there a way to use decide anyway here?

theorem test (x:Nat) (q: x=3): x+1=4 := by decide

[Kyle Miller]

Use subst_vars before running decide (or, rather, rfl)

[Simon Daniel]

thanks!