cases h₀:s₀ <;> cases h₁:s₁
s₀ s₁ : Source
⊢ encodeSource s₀ = encodeSource s₁ → s₀ = s₁
case nil.nil
s₀ s₁ : Source
h₀ : s₀ = Source.nil
h₁ : s₁ = Source.nil
⊢ encodeSource Source.nil = encodeSource Source.nil → Source.nil = Source.nil

case nil.imm
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.imm hd✝ tl✝) → Source.nil = Source.imm hd✝ tl✝

case nil.idx
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.idx hd✝ tl✝) → Source.nil = Source.idx hd✝ tl✝

case imm.nil
s₀ s₁ : Source
hd✝ : Bool
tl✝ : Source
h₀ : s₀ = Source.imm hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.imm hd✝ tl✝) = encodeSource Source.nil → Source.imm hd✝ tl✝ = Source.nil

case imm.imm
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.imm hd✝ tl✝

case imm.idx
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.idx hd✝ tl✝

case idx.nil
s₀ s₁ hd✝ tl✝ : Source
h₀ : s₀ = Source.idx hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.idx hd✝ tl✝) = encodeSource Source.nil → Source.idx hd✝ tl✝ = Source.nil

case idx.imm
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.imm hd✝ tl✝

case idx.idx
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.idx hd✝ tl✝