Function concat_empty 

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

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

(open)

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