no goals
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
L R : List Γ
⊢ map f (mk₂ L R) = mk₂ (List.map f.f L) (List.map f.f R)
simp only [Tape.mk₂, Tape.map_mk', ListBlank.map_mk]