a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
⊢ x ≠ Γ'.consₗ
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList (a :: l)
⊢ x ≠ Γ'.consₗ
simp [trList] at h
case inl
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a
⊢ x ≠ Γ'.consₗ

case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ

case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
⊢ x ≠ Γ'.consₗ
obtain h | rfl | h := h
case inl
a : ℕ
l : List ℕ
h : Γ'.consₗ ∈ trNat a
⊢ False
case inl
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a
⊢ x ≠ Γ'.consₗ
rintro rfl
no goals
case inl
a : ℕ
l : List ℕ
h : Γ'.consₗ ∈ trNat a
⊢ False
cases trNat_natEnd _ _ h
no goals
case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ
rintro ⟨⟩
no goals
case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ
exact trList_ne_consₗ l _ h