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