case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ write { head := head✝, left := left✝, right := right✝ }.head { head := head✝, left := left✝, right := right✝ } =
    { head := head✝, left := left✝, right := right✝ }
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ ∀ (T : Tape Γ), write T.head T = T
rintro ⟨⟩
no goals
case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ write { head := head✝, left := left✝, right := right✝ }.head { head := head✝, left := left✝, right := right✝ } =
    { head := head✝, left := left✝, right := right✝ }
rfl