have : a ∈ as ∧ as' ⊆ as := by simpa using has
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
this : a ∈ as ∧ as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'