Draft: Predicate `list.Sorted.sorted` recursively-defined.

I believe that predicate list.Sorted.sorted remains an inductive definition for historical reasons.

Since we can attach variant to logical symbols, such predicate can be easily defined recursively, as follows:

  let rec ghost predicate sorted (l: list t)
    variant { l }
  = match l with
    | Nil | Cons _ Nil -> true
    | Cons x (Cons y l) ->
        le x y && sorted (Cons y l)
    end

A quick grep shows that list.Sorted is used in seven different examples:

• coincidence_count_list
• insertion_sort_list
• mergesort_list
• sorted_list
• tower_of_hanoi
• verifythis_2019_cartesian_trees
• verifythis_2019_ghc_sort

With this new definition of sorted, the only proofs that remain to be ported are verifythis_2019_cartesian_trees and _cartesian_trees (both authored by @qgarcher ). However, I do not do believe such proofs are stuck due to the new definition of sorted. The first one seems to be an issue with detached nodes of interactive proof; the second one seems to be some trick invariants and a postcondition with an existential quantifier.