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