no goals
Γ : Type u_1
inst✝ : Inhabited Γ
a b : Γ
L R : ListBlank Γ
⊢ write b (mk' L (ListBlank.cons a R)) = mk' L (ListBlank.cons b R)
simp only [Tape.write, Tape.mk', ListBlank.head_cons, ListBlank.tail_cons, eq_self_iff_true,
  and_self_iff]