pub broadcast proof fn axiom_increasing_seq_meaning<K: Ord>(s: Seq<K>)Expand description
requires
obeys_cmp_spec::<K>(),#[trigger] increasing_seq(s)
<==> forall |i, j| 0 <= i < j < s.len() ==> s[i].cmp_spec(&s[j]) is Less,An interpretation for the increasing_seq predicate.