α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a = head✝.fst ∧ ¬a ∈ keys l₁
⊢ kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a ∈ keys (head✝ :: l₁)
⊢ kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂
simp [not_or] at h
no goals
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a = head✝.fst ∧ ¬a ∈ keys l₁
⊢ kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂
simp [h.1, kerase_append_right h.2]