no goals
K : Type ?u.595576
inst✝² : DecidableEq K
Γ : K → Type ?u.595590
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L : ListBlank ((k : K) → Option (Γ k))
⊢ default.snd = default
rfl
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.cons (ListBlank.head L)
      (ListBlank.map { f := Prod.snd, map_pt' := (_ : default.snd = default.snd) }
        (ListBlank.map { f := Prod.mk false, map_pt' := (_ : (false, default) = (false, default)) }
          (ListBlank.tail L))) =
    L
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := (_ : default.snd = default.snd) } (addBottom L) = L
simp only [addBottom, ListBlank.map_cons]
case h.e'_2.h.e'_4
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := (_ : default.snd = default.snd) }
      (ListBlank.map { f := Prod.mk false, map_pt' := (_ : (false, default) = (false, default)) } (ListBlank.tail L)) =
    ListBlank.tail L
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.cons (ListBlank.head L)
      (ListBlank.map { f := Prod.snd, map_pt' := (_ : default.snd = default.snd) }
        (ListBlank.map { f := Prod.mk false, map_pt' := (_ : (false, default) = (false, default)) }
          (ListBlank.tail L))) =
    L
convert ListBlank.cons_head_tail L
case h.e'_2.h.e'_4
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L L' : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := (_ : default.snd = default.snd) }
      (ListBlank.map { f := Prod.mk false, map_pt' := (_ : (false, default) = (false, default)) } L') =
    L'
case h.e'_2.h.e'_4
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := (_ : default.snd = default.snd) }
      (ListBlank.map { f := Prod.mk false, map_pt' := (_ : (false, default) = (false, default)) } (ListBlank.tail L)) =
    ListBlank.tail L
generalize ListBlank.tail L = L'
case h.e'_2.h.e'_4
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L L' : ListBlank ((k : K) → Option (Γ k))
l : List ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := (_ : default.snd = default.snd) }
      (ListBlank.map { f := Prod.mk false, map_pt' := (_ : (false, default) = (false, default)) } (ListBlank.mk l)) =
    ListBlank.mk l
case h.e'_2.h.e'_4
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L L' : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := (_ : default.snd = default.snd) }
      (ListBlank.map { f := Prod.mk false, map_pt' := (_ : (false, default) = (false, default)) } L') =
    L'
refine' L'.induction_on fun l ↦ _
no goals
case h.e'_2.h.e'_4
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.595593
inst✝¹ : Inhabited Λ
σ : Type ?u.595599
inst✝ : Inhabited σ
L L' : ListBlank ((k : K) → Option (Γ k))
l : List ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := (_ : default.snd = default.snd) }
      (ListBlank.map { f := Prod.mk false, map_pt' := (_ : (false, default) = (false, default)) } (ListBlank.mk l)) =
    ListBlank.mk l
simp