case imm.imm => simpa [encodeSource] using λ hhd htl ↦ ⟨hhd, encodeSource_inj htl⟩
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✝
no goals