α : Sort u_1
ctx : Context α
x : Nat
⊢ (match (var ctx x).neutral with
      | some val => true
      | none => false) =
      true →
    IsNeutral ctx.op (var ctx x).value
α : Sort u_1
ctx : Context α
x : Nat
⊢ ContextInformation.isNeutral ctx x = true → IsNeutral (EvalInformation.evalOp ctx) (EvalInformation.evalVar ctx x)
simp [ContextInformation.isNeutral, Option.isSome, EvalInformation.evalOp, EvalInformation.evalVar]
no goals
α : Sort u_1
ctx : Context α
x : Nat
⊢ (match (var ctx x).neutral with
      | some val => true
      | none => false) =
      true →
    IsNeutral ctx.op (var ctx x).value
match (var ctx x).neutral with
| some hn => intro; assumption
| none => intro; contradiction
α : Sort u_1
ctx : Context α
x : Nat
hn : IsNeutral ctx.op (var ctx x).value
a✝ :
  (match some hn with
    | some val => true
    | none => false) =
    true
⊢ IsNeutral ctx.op (var ctx x).value
α : Sort u_1
ctx : Context α
x : Nat
hn : IsNeutral ctx.op (var ctx x).value
⊢ (match some hn with
      | some val => true
      | none => false) =
      true →
    IsNeutral ctx.op (var ctx x).value
intro
no goals
α : Sort u_1
ctx : Context α
x : Nat
hn : IsNeutral ctx.op (var ctx x).value
a✝ :
  (match some hn with
    | some val => true
    | none => false) =
    true
⊢ IsNeutral ctx.op (var ctx x).value
assumption
α : Sort u_1
ctx : Context α
x : Nat
a✝ :
  (match none with
    | some val => true
    | none => false) =
    true
⊢ IsNeutral ctx.op (var ctx x).value
α : Sort u_1
ctx : Context α
x : Nat
⊢ (match none with
      | some val => true
      | none => false) =
      true →
    IsNeutral ctx.op (var ctx x).value
intro
no goals
α : Sort u_1
ctx : Context α
x : Nat
a✝ :
  (match none with
    | some val => true
    | none => false) =
    true
⊢ IsNeutral ctx.op (var ctx x).value
contradiction