Theorem: Lean4Lean.VEnv.IsDefEqStrong.weak0 (Lean4Lean/Theory/Typing/Strong.lean)

State before:
env : VEnv
henv : Ordered env
U : Nat
e1 e2 A : VExpr
Γ : List VExpr
H : IsDefEqStrong env U [] e1 e2 A
⊢ IsDefEqStrong env U Γ e1 e2 A
Tactic:
have ⟨h1, h2, h3⟩ := H.defeq.closedN' henv.closed ⟨⟩
State after:
env : VEnv
henv : Ordered env
U : Nat
e1 e2 A : VExpr
Γ : List VExpr
H : IsDefEqStrong env U [] e1 e2 A
h1 : ClosedN e1 (List.length [])
h2 : ClosedN e2 (List.length [])
h3 : ClosedN A (List.length [])
⊢ IsDefEqStrong env U Γ e1 e2 A

State before:
env : VEnv
henv : Ordered env
U : Nat
e1 e2 A : VExpr
Γ : List VExpr
H : IsDefEqStrong env U [] e1 e2 A
h1 : ClosedN e1 (List.length [])
h2 : ClosedN e2 (List.length [])
h3 : ClosedN A (List.length [])
⊢ IsDefEqStrong env U Γ e1 e2 A
Tactic:
simpa [h1.liftN_eq (Nat.zero_le _), h2.liftN_eq (Nat.zero_le _),
  h3.liftN_eq (Nat.zero_le _)] using H.weakN henv (.zero Γ rfl)
State after:
no goals