Theorem: type_correct (STLC.lean)

State before:
ctx : Ctx
t : Term
ty : Ty
h : type ctx t = some ty
⊢ ctx ⊢ t ⋮ ty
Tactic:
induction t generalizing ty ctx <;> simp [type, bind, Option.bind] at h
State after:
case var
fvar✝ : Nat
ctx : Ctx
ty : Ty
h : ctx fvar✝ = some ty
⊢ ctx ⊢ Term.var fvar✝ ⋮ ty

case abs
ty✝ : Ty
body✝ : Term
body_ih✝ : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type (↥ctx)[0 ↦ ty✝] body✝, fun __do_lift => pure (Ty.arrow ty✝ __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty

case app
t₁✝ t₂✝ : Term
t₁_ih✝ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁✝ = some ty → ctx ⊢ t₁✝ ⋮ ty
t₂_ih✝ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂✝ = some ty → ctx ⊢ t₂✝ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type ctx t₁✝ with
    | some (Ty.arrow ty₁ ty₂) =>
      match type ctx t₂✝, fun __do_lift => if ty₁ = __do_lift then some ty₂ else none with
      | none, x => none
      | some a, b => b a
    | x => none) =
    some ty
⊢ ctx ⊢ Term.app t₁✝ t₂✝ ⋮ ty

State before:
fvar✝ : Nat
ctx : Ctx
ty : Ty
h : ctx fvar✝ = some ty
⊢ ctx ⊢ Term.var fvar✝ ⋮ ty
Tactic:
case var => exact .var h
State after:
no goals

State before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type (↥ctx)[0 ↦ ty✝] body✝, fun __do_lift => pure (Ty.arrow ty✝ __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
case abs hi => 
  split at h <;> try contradiction
  case _ ht =>
    simp [pure] at h
    subst h
    exact .abs (hi ht)
State after:
no goals

State before:
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type ctx t₁ with
    | some (Ty.arrow ty₁ ty₂) =>
      match type ctx t₂, fun __do_lift => if ty₁ = __do_lift then some ty₂ else none with
      | none, x => none
      | some a, b => b a
    | x => none) =
    some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
case app t₁ t₂ hi₁ hi₂ =>
  cases h₁ : type ctx t₁ <;> cases h₂ : type ctx t₂ <;> simp_all [h₁, h₂]
  all_goals split at h <;> try contradiction
  case _ ty₁ ty₂ _ ty₁₁ _ ha =>
    specialize hi₁ h₁
    split at h <;> simp_all
    exact .app hi₁ (hi₂ h₂)
State after:
no goals

State before:
fvar✝ : Nat
ctx : Ctx
ty : Ty
h : ctx fvar✝ = some ty
⊢ ctx ⊢ Term.var fvar✝ ⋮ ty
Tactic:
exact .var h
State after:
no goals

State before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type (↥ctx)[0 ↦ ty✝] body✝, fun __do_lift => pure (Ty.arrow ty✝ __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
split at h <;> try contradiction
State after:
case h_2
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
heq✝ : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : (fun __do_lift => pure (Ty.arrow ty✝ __do_lift)) a✝ = some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty

State before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : (fun __do_lift => pure (Ty.arrow ty✝ __do_lift)) a✝ = some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
case _ ht =>
  simp [pure] at h
  subst h
  exact .abs (hi ht)
State after:
no goals

State before:
case h_1
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
heq✝ : type (↥ctx)[0 ↦ ty✝] body✝ = none
h : none = some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
contradiction
State after:
no goals

State before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : (fun __do_lift => pure (Ty.arrow ty✝ __do_lift)) a✝ = some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
simp [pure] at h
State after:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : Ty.arrow ty✝ a✝ = ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty

State before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : Ty.arrow ty✝ a✝ = ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
subst h
State after:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ Ty.arrow ty✝ a✝

State before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ Ty.arrow ty✝ a✝
Tactic:
exact .abs (hi ht)
State after:
no goals

State before:
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type ctx t₁ with
    | some (Ty.arrow ty₁ ty₂) =>
      match type ctx t₂, fun __do_lift => if ty₁ = __do_lift then some ty₂ else none with
      | none, x => none
      | some a, b => b a
    | x => none) =
    some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
cases h₁ : type ctx t₁ <;> cases h₂ : type ctx t₂ <;> simp_all [h₁, h₂]
State after:
case some.none
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝ : Ty
h :
  (match some val✝ with
    | some (Ty.arrow ty₁ ty₂) => none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝
h₂ : type ctx t₂ = none
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

case some.some
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h :
  (match some val✝¹ with
    | some (Ty.arrow ty₁ ty₂) => if ty₁ = val✝ then some ty₂ else none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

State before:
case some.none
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝ : Ty
h :
  (match some val✝ with
    | some (Ty.arrow ty₁ ty₂) => none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝
h₂ : type ctx t₂ = none
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

case some.some
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h :
  (match some val✝¹ with
    | some (Ty.arrow ty₁ ty₂) => if ty₁ = val✝ then some ty₂ else none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
all_goals split at h <;> try contradiction
State after:
case some.some.h_1
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
x✝ : Option Ty
ty₁✝ ty₂✝ : Ty
heq✝ : some val✝¹ = some (Ty.arrow ty₁✝ ty₂✝)
h : (if ty₁✝ = val✝ then some ty₂✝ else none) = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

State before:
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₁ : type ctx t₁ = some ty₁
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
ha : some ty₁ = some (Ty.arrow ty₁₁ ty₂✝)
h : (if ty₁₁ = ty₂ then some ty₂✝ else none) = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
case _ ty₁ ty₂ _ ty₁₁ _ ha =>
  specialize hi₁ h₁
  split at h <;> simp_all
  exact .app hi₁ (hi₂ h₂)
State after:
no goals

State before:
case some.some
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h :
  (match some val✝¹ with
    | some (Ty.arrow ty₁ ty₂) => if ty₁ = val✝ then some ty₂ else none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
split at h <;> try contradiction
State after:
case some.some.h_1
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
x✝ : Option Ty
ty₁✝ ty₂✝ : Ty
heq✝ : some val✝¹ = some (Ty.arrow ty₁✝ ty₂✝)
h : (if ty₁✝ = val✝ then some ty₂✝ else none) = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

State before:
case some.some.h_2
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
x✝¹ : Option Ty
x✝ : ∀ (ty₁ ty₂ : Ty), some val✝¹ = some (Ty.arrow ty₁ ty₂) → False
h : none = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
contradiction
State after:
no goals

State before:
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₁ : type ctx t₁ = some ty₁
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
ha : some ty₁ = some (Ty.arrow ty₁₁ ty₂✝)
h : (if ty₁₁ = ty₂ then some ty₂✝ else none) = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
specialize hi₁ h₁
State after:
t₁ t₂ : Term
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₁ : type ctx t₁ = some ty₁
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
ha : some ty₁ = some (Ty.arrow ty₁₁ ty₂✝)
h : (if ty₁₁ = ty₂ then some ty₂✝ else none) = some ty
hi₁ : ctx ⊢ t₁ ⋮ ty₁
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

State before:
t₁ t₂ : Term
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₁ : type ctx t₁ = some ty₁
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
ha : some ty₁ = some (Ty.arrow ty₁₁ ty₂✝)
h : (if ty₁₁ = ty₂ then some ty₂✝ else none) = some ty
hi₁ : ctx ⊢ t₁ ⋮ ty₁
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
split at h <;> simp_all
State after:
case inl
t₁ t₂ : Term
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
hi₁ : ctx ⊢ t₁ ⋮ Ty.arrow ty₂ ty
h✝ : ty₁₁ = ty₂
h : ty₂✝ = ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

State before:
case inl
t₁ t₂ : Term
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
hi₁ : ctx ⊢ t₁ ⋮ Ty.arrow ty₂ ty
h✝ : ty₁₁ = ty₂
h : ty₂✝ = ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
exact .app hi₁ (hi₂ h₂)
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
h : ctx ⊢ t ⋮ ty
⊢ type ctx t = some ty
Tactic:
induction h <;> simp [type]
State after:
case var
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
⊢ ctx✝ x✝ = some ty✝

case abs
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← type (↥ctx✝)[0 ↦ ty₁✝] t✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)

case app
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
a_ih✝ : type ctx✝ t₂✝ = some ty₁✝
⊢ (match type ctx✝ t₁✝ with
    | some (Ty.arrow ty₁ ty₂) => do
      let __do_lift ← type ctx✝ t₂✝
      if ty₁ = __do_lift then some ty₂ else none
    | x => none) =
    some ty₂✝

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
⊢ ctx✝ x✝ = some ty✝
Tactic:
case var         => assumption
State after:
no goals

State before:
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← type (↥ctx✝)[0 ↦ ty₁✝] t✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)
Tactic:
case abs hi      => rw [hi]; rfl
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (match type ctx✝ t₁✝ with
    | some (Ty.arrow ty₁ ty₂) => do
      let __do_lift ← type ctx✝ t₂✝
      if ty₁ = __do_lift then some ty₂ else none
    | x => none) =
    some ty₂✝
Tactic:
case app hi₁ hi₂ => simp [hi₁, hi₂]; exact if_pos rfl
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
⊢ ctx✝ x✝ = some ty✝
Tactic:
assumption
State after:
no goals

State before:
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← type (↥ctx✝)[0 ↦ ty₁✝] t✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)
Tactic:
rw [hi]
State after:
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← some ty₂✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)

State before:
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← some ty₂✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)
Tactic:
rfl
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (match type ctx✝ t₁✝ with
    | some (Ty.arrow ty₁ ty₂) => do
      let __do_lift ← type ctx✝ t₂✝
      if ty₁ = __do_lift then some ty₂ else none
    | x => none) =
    some ty₂✝
Tactic:
simp [hi₁, hi₂]
State after:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (do
      let __do_lift ← some ty₁✝
      if ty₁✝ = __do_lift then some ty₂✝ else none) =
    some ty₂✝

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (do
      let __do_lift ← some ty₁✝
      if ty₁✝ = __do_lift then some ty₂✝ else none) =
    some ty₂✝
Tactic:
exact if_pos rfl
State after:
no goals