example (a b : nat) : a = b → a = b :=
begin
  intro,
  assumption
end