exact Nat.lt_succ.mpr (Nat.left_le_pair (encode b) (encode 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
no goals