Comencé haciendo intros, dando como testigo a (insert_sort l) y aplicando functional iduction sobre el testigo. El paso base lo logré probar pero luego tengo que dar una prueba de lo siguiente:
2 subgoals
A : Set
x : nat
xl : list nat
IHl0 : sorted nat le (insert_sort xl) /\ perm nat xl (insert_sort xl)
H : sorted nat le (insert_sort xl)
H0 : perm nat xl (insert_sort xl)
______________________________________(1/2)
sorted nat le (insert x (insert_sort xl))
No veo como poder usar las hipótesis para realizar la prueba. Alguna sugerencia?
Gracias.