Theorem depending on lemma using `include`

Stream: new members

[Aron Erben]

Hello, I have this MWE (the proof itself is not important, this is merely a syntax question):

variables
  {a : ℕ}
  {h : 1 = a}

include a h
lemma two_eq_one_plus_one : a = 1 :=
begin
  exact symm h,
end

theorem three_eq_two_plus_one : 2 = a + 1 :=
begin
  -- Error is here
  rw two_eq_one_plus_one,
end

The theorem depends on the lemma and the lemma includes two variables. This does not compile and gives the following error:

13:3: rewrite tactic failed, lemma lhs is a metavariable
state:
a : ℕ,
h : 1 = a
⊢ 2 = a + 1

I'm not entirely sure what the error is, I suspect it's because a is converted to an implicit arg and is referenced on the lhs? I found two ways to fix it:

1. Either by listing the implicit args:

theorem three_eq_two_plus_one : 2 = a + 1 :=
begin
  rw @two_eq_one_plus_one a h,
end

2. Wrapping everything into a section and using parameters:

section
parameters
  {a : ℕ}
  {h : 1 = a}
...
end

I'm not really happy with either, is there something else I could do?
Thanks in advance!

[Ruben Van de Velde]

Well, it's just that lean can't figure out what a is - it could equally well be 2 or a + 1 or 1. I don't think it makes sense for both a and h to be implicit in two_eq_one_plus_one

[Ruben Van de Velde]

Any time you try to rewrite with an equality whose left hand side is a bare variable, you'll hit this error (unless you tell lean what the variable should be)

[Aron Erben]

Ruben Van de Velde said:

Well, it's just that lean can't figure out what a is - it could equally well be 2 or a + 1 or 1. I don't think it makes sense for both a and h to be implicit in two_eq_one_plus_one

Ah I see, that makes sense. Do you think this is a cleaner, more canonical solution:

variables
  {a : ℕ}
  (h : 1 = a)

include a h
lemma two_eq_one_plus_one : a = 1 :=
begin
  exact symm h,
end

theorem three_eq_two_plus_one : 2 = a + 1 :=
begin
  rw two_eq_one_plus_one h,
end

[Ruben Van de Velde]

I think that makes more sense, yes