Theorem: Lean4Lean.Lookup.lt (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
Γ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ i A
⊢ i < List.length Γ
Tactic:
induction H with
| zero => apply Nat.succ_pos
| succ _ ih => apply Nat.succ_lt_succ ih
State after:
no goals

State before:
case zero
Γ : List VExpr
i : Nat
A ty✝ : VExpr
Γ✝ : List VExpr
⊢ 0 < List.length (ty✝ :: Γ✝)
Tactic:
apply Nat.succ_pos
State after:
no goals

State before:
case succ
Γ : List VExpr
i : Nat
A : VExpr
Γ✝ : List VExpr
n✝ : Nat
ty✝ A✝ : VExpr
a✝ : Lookup Γ✝ n✝ ty✝
ih : n✝ < List.length Γ✝
⊢ n✝ + 1 < List.length (A✝ :: Γ✝)
Tactic:
apply Nat.succ_lt_succ ih
State after:
no goals