inductive IsEven : Nat → Prop| zero : IsEven 0| succ : ∀ n, IsEven n → IsEven (n + 2)def IsEvenProp (p : Nat → Prop) : Prop :=  p 0 ∧ (∀ n, p n → p (n + 2))theorem IsEvenPropOfIsEven : IsEvenProp IsEven := by  unfold IsEvenProp  constructor  · exact IsEven.zero  · intro n h    exact IsEven.succ n h/--least fixed point of IsEvenProp.See that this uses impredicativity.It is quantifying over all (p : Nat → Prop).In doing so, it is quantifying over *itself* (IsEven' : Nat → Prop).-/def IsEven' : Nat → Prop := fun n =>  ∀ (p : Nat → Prop) (hp : IsEvenProp p), p ntheorem IsEven'_zero : IsEven' 0 := by  intro p hp  unfold IsEvenProp at hp  obtain ⟨h0, _hsucc⟩ := hp  exact h0theorem IsEven'_ind (h : IsEven' n) : IsEven' (n + 2) := by  intro p hp  unfold IsEvenProp at hp  obtain ⟨h0, hsucc⟩ := hp  apply hsucc  unfold IsEven' at h  apply h  unfold IsEvenProp  simp only  constructor <;> assumption<;><;><;>theorem IsEvenOfIsEven' : ∀ n, IsEven' n → IsEven n := by<;>  unfold IsEven'<;>  intros n<;>  intros h<;>  specialize h IsEven IsEvenPropOfIsEven<;>  exact h<;><;>theorem IsEven'OfIsEven : ∀ n, IsEven n → IsEven' n := by<;>  intro n<;>  intros h<;>  induction h<;>  case zero => exact IsEven'_zero<;>  case succ m heven heven' =><;>    exact IsEven'_ind heven'<;><;>theorem IsEven_eq_IsEven' : ∀ n, IsEven n ↔ IsEven' n := by<;>  intro n<;>  apply Iff.intro<;>  · apply IsEven'OfIsEven<;>  · apply IsEvenOfIsEven'