Function concat_empty

pub fn concat_empty<T>(s: FSet<Seq<T>>)

The neutral element of FSet::concat is FSet::singleton(Seq::EMPTY).

logic

proof_assert! { forall<xs: Seq<T>> xs.concat(Seq::EMPTY) == xs };
proof_assert! { forall<xs: Seq<T>> Seq::EMPTY.concat(xs) == xs };

ensures

FSet::concat(FSet::singleton(Seq::EMPTY), s) == s

ensures

FSet::concat(s, FSet::singleton(Seq::EMPTY)) == s