うーむ，variableで宣言した変数が，theorem以下ではnot foundと言われてしまう。
section test
theorem T
(a b c d e : Nat)
(h1 : a = b)
(h2 : b = c + 1)
(h3 : c = d)
(h4 : e = 1 + d)
: a = e :=
calc
a = b := h1
b = c + 1 := h2
c + 1 = d + 1 := congrArg Nat.succ h3
d + 1 = 1 + d := Nat.add_comm d 1
1 + d = e := Eq.symm h4
end testしょうがない。ということでtheoremの中で変数宣言したら動いた。
