Theorem: LambdaCalculi.concat_hasType (LambdaCalculi/HasType.lean)

State before:
p : LambdaParams
U : Type u_2
C : Type ?u.1008396
C✝ : Type u_1
T : C✝ → LambdaType p U
Γ : Context p U
t : LambdaTerm p U C✝
σ : LambdaType p U
h : Γ ⊢[T] t ∶ σ
τ : LambdaType p U
⊢ List.concat Γ τ ⊢[T] t ∶ σ
Tactic:
rw [List.concat_eq_append]
State after:
p : LambdaParams
U : Type u_2
C : Type ?u.1008396
C✝ : Type u_1
T : C✝ → LambdaType p U
Γ : Context p U
t : LambdaTerm p U C✝
σ : LambdaType p U
h : Γ ⊢[T] t ∶ σ
τ : LambdaType p U
⊢ Γ ++ [τ] ⊢[T] t ∶ σ

State before:
p : LambdaParams
U : Type u_2
C : Type ?u.1008396
C✝ : Type u_1
T : C✝ → LambdaType p U
Γ : Context p U
t : LambdaTerm p U C✝
σ : LambdaType p U
h : Γ ⊢[T] t ∶ σ
τ : LambdaType p U
⊢ Γ ++ [τ] ⊢[T] t ∶ σ
Tactic:
exact append_hasType h [τ]
State after:
no goals