Theorem: Lean4Lean.VEnv.IsDefEq.trans_l (Lean4Lean/Theory/Typing/UniqueTyping.lean)

State before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A e₃ B : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEq env U Γ e₁ e₂ A
h₂ : IsDefEq env U Γ e₂ e₃ B
⊢ IsDefEq env U Γ e₁ e₃ A
Tactic:
have ⟨_, h⟩ := h₁.uniq henv hΓ h₂
State after:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A e₃ B : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEq env U Γ e₁ e₂ A
h₂ : IsDefEq env U Γ e₂ e₃ B
w✝ : VLevel
h : IsDefEq env U Γ A B (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₃ A

State before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A e₃ B : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEq env U Γ e₁ e₂ A
h₂ : IsDefEq env U Γ e₂ e₃ B
w✝ : VLevel
h : IsDefEq env U Γ A B (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₃ A
Tactic:
exact h₁.trans (.defeqDF (.symm h) h₂)
State after:
no goals