def even2 : sorry :=
  have e : 1 + 1 = 2 := Eq.refl _
  sorry