Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
⊢ cons (head (map f (cons a l))) (tail (map f (cons a l))) = cons (PointedMap.f f a) (map f l)
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
⊢ map f (cons a l) = cons (PointedMap.f f a) (map f l)
refine' (ListBlank.cons_head_tail _).symm.trans _
no goals
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
⊢ cons (head (map f (cons a l))) (tail (map f (cons a l))) = cons (PointedMap.f f a) (map f l)
simp only [ListBlank.head_map, ListBlank.head_cons, ListBlank.tail_map, ListBlank.tail_cons]