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

State before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B : VExpr
henv : Ordered env
hΓ : CtxStrong env U Γ
h1 : IsDefEqStrong env U Γ A A' (sort u)
h2 : IsDefEqStrong env U (A :: Γ) e1 e2 B
⊢ IsDefEqStrong env U (A' :: Γ) e1 e2 B
Tactic:
simpa [instN_bvar0] using
  have hu := h1.defeq.sort_r henv hΓ.defeq
  have hΓ' := ⟨hΓ, _, h1.hasType.2⟩
  h1.weakN henv (.one (A := A'))
    |>.symm.defeqDF hu (.bvar .zero hu (h1.hasType.2.weakN henv .one))
    |>.instN henv hΓ' .zero (h2.weakN henv (.succ (.one (A := A')))) hΓ'
State after:
no goals