fact: Definition FiniteSetSig : ADTSig := ADTsignature { Constructor sEmpty : unit -> rep, Method sAdd : rep x W -> rep x unit, Method sRemove : rep x W -> rep x unit, Method sIn : rep x W -> rep x bool, Method sSize : rep x unit -> rep x W }.
imports: Coq.Sets.Ensembles Fiat.ADT.Core Fiat.Common.Ensembles Fiat.ADT.ComputationalADT Fiat.ADTNotation Fiat.FiniteSetADTs.BedrockWord