no goals
c : Code
n x : ℕ
h : x ∈ evaln 0 c n
⊢ n < 0
simp [evaln] at h
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ n < k + 1
suffices ∀ {o : Option ℕ}, x ∈ do { guard (n ≤ k); o } → n < k + 1 by
  cases c <;> rw [evaln] at h <;> exact this h
no goals
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
simpa [Bind.bind] using Nat.lt_succ_of_le
no goals
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
⊢ n < k + 1
cases c <;> rw [evaln] at h <;> exact this h