constant  c : ℕ
constants (d e : ℕ) (f : ℕ → ℕ)
axiom     cd_eq : c = d
 
def foo : ℕ := 5
def bar := 6
def baz (x y : ℕ) (s : list ℕ) := [x, y] ++ s
 
theorem foo_eq_five : foo = 5 := rfl
theorem baz_theorem (x y : ℕ) : baz x y [] = [x, y] := rfl
lemma baz_lemma (x y : ℕ) : baz x y [] = [x, y] := rfl
 
example (x y : ℕ) : baz x y [] = [x, y] := rfl