insert x (b :: l) reduces to if x <=? b then x :: b :: l else b :: insert x l, which is not b :: insert x l. You can simplify IHIHl to make the latter term appear, get a proof that x <=? b = true from E' : b < x and rewrite this proof in IHIHl to make the term reduce further.