Theorem: Lean4Lean.VEnv.IsDefEq.weakR (Lean4Lean/Theory/Typing/Lemmas.lean)

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

State before:
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
hΓ : CtxClosed Γ
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
h1 : ClosedN e1 (List.length Γ)
h2 : ClosedN e2 (List.length Γ)
h3 : ClosedN A (List.length Γ)
⊢ IsDefEq env U (Γ ++ Γ') e1 e2 A
Tactic:
simpa [h1.liftN_eq, h2.liftN_eq, h3.liftN_eq] using H.weakN henv (.right hΓ Γ')
State after:
no goals