case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ mk' { head := head✝, left := left✝, right := right✝ }.left
      (right₀ { head := head✝, left := left✝, right := right✝ }) =
    { head := head✝, left := left✝, right := right✝ }
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ mk' T.left (right₀ T) = T
cases T
no goals
case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ mk' { head := head✝, left := left✝, right := right✝ }.left
      (right₀ { head := head✝, left := left✝, right := right✝ }) =
    { head := head✝, left := left✝, right := right✝ }
simp only [Tape.right₀, Tape.mk', ListBlank.head_cons, ListBlank.tail_cons, eq_self_iff_true,
  and_self_iff]