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

State before:
p : LambdaParams
U : Type ?u.1008897
C : Type ?u.1008900
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ (List.concat Γ τ ⊢[T] t ∶ σ) ↔ (Γ ⊢[T] t ∶ σ)
Tactic:
rw [List.concat_eq_append]
State after:
p : LambdaParams
U : Type ?u.1008897
C : Type ?u.1008900
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ (Γ ++ [τ] ⊢[T] t ∶ σ) ↔ (Γ ⊢[T] t ∶ σ)

State before:
p : LambdaParams
U : Type ?u.1008897
C : Type ?u.1008900
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ (Γ ++ [τ] ⊢[T] t ∶ σ) ↔ (Γ ⊢[T] t ∶ σ)
Tactic:
exact append_hasType_iff ht
State after:
no goals