case h
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ ∀ (a : List Γ), cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a)) = Quotient.mk'' a
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ ∀ (l : ListBlank Γ), cons (head l) (tail l) = l
apply Quotient.ind'
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
⊢ BlankExtends l (head (Quotient.mk'' l) :: List.tail l)
case h
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ ∀ (a : List Γ), cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a)) = Quotient.mk'' a
refine' fun l ↦ Quotient.sound' (Or.inr _)
case h.nil
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ BlankExtends [] (head (Quotient.mk'' []) :: List.tail [])

case h.cons
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝) (head (Quotient.mk'' (head✝ :: tail✝)) :: List.tail (head✝ :: tail✝))
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
⊢ BlankExtends l (head (Quotient.mk'' l) :: List.tail l)
cases l
no goals
case h.nil
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ BlankExtends [] (head (Quotient.mk'' []) :: List.tail [])
exact ⟨1, rfl⟩
no goals
case h.cons
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝) (head (Quotient.mk'' (head✝ :: tail✝)) :: List.tail (head✝ :: tail✝))
rfl