Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
M : Λ → Stmt₁
l : List Γ
⊢ Part.map ((fun c => Tape.right₀ c.Tape) ∘ fun a => trCfg M a)
      (eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) =
    Part.map (fun c => Tape.right₀ c.Tape) (eval (TM1.step M) (TM1.init l))
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
M : Λ → Stmt₁
l : List Γ
⊢ Part.map (fun c => Tape.right₀ c.Tape)
      ((fun a => trCfg M a) <$> eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) =
    TM1.eval M l
rw [Part.map_eq_map, Part.map_map, TM1.eval]
no goals
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
M : Λ → Stmt₁
l : List Γ
⊢ Part.map ((fun c => Tape.right₀ c.Tape) ∘ fun a => trCfg M a)
      (eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) =
    Part.map (fun c => Tape.right₀ c.Tape) (eval (TM1.step M) (TM1.init l))
congr with ⟨⟩