Theorem: Lean4Lean.VEnv.IsDefEqU.weakN_iff (Lean4Lean/Theory/Typing/UniqueTyping.lean)

State before:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
n k : Nat
Γ : List VExpr
e1 e2 : VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqU env U Γ' (VExpr.liftN n e1 k) (VExpr.liftN n e2 k) ↔ IsDefEqU env U Γ e1 e2
Tactic:
refine ⟨fun h => have := henv; have := hΓ; sorry, fun h => h.weakN henv W⟩
State after:
no goals