rcases this with (rfl | lt) <;> simp
case cons
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
this : b = b' ∨ b ∈ bs
⊢ encode b < encode (b' :: bs)
case cons.inl
β : Type u_1
inst✝ : Encodable β
b : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b :: bs
⊢ encode b < (encode b).pair (encode bs) + 1

case cons.inr
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
lt : b ∈ bs
⊢ encode b < (encode b').pair (encode bs) + 1