Software Foundations/ Verified Functional Algorithms Ejercicio

[es] ¡Coq en español!
1

Hola buenas, he estado intentando resolver los ejercicios de la parte de merge del libro Verified Functional Algorithms y estoy teniendo un problema con uno.
Lemma sorted_merge : forall l1, sorted l1 ->
forall l2, sorted l2 ->
sorted (merge l1 l2).
Proof.

intros. induction l1.

  • simpl. induction l2.
    • auto.
    • auto.
  • induction l2.
    • auto.
    • simpl. bdestruct (a<=?a0).
      • inv H.
        ** auto. constructor. auto. auto.
        ** apply sorted_merge1. auto. auto. auto.

Esto es lo que he conseguido hacer. Supongo que ahora tendré que hacer otra inducción en l2 pero haciendo eso solo me complico más.

Muchas gracias