Setoids are algebraic structures characterised by a domain and an equality relation.
** Module lib_setoid Imports parameters $Setoid : Type(Setoid) $make_Setoid : {dom:Type}(dom->dom->Prop)->Setoid $Setoid_elim : {C_Setoid:Setoid->TYPE} ({dom:Type}{eq1:dom->dom->Prop}C_Setoid (make_Setoid dom eq1))-> {z:Setoid}C_Setoid z [[C_Setoid:Setoid->TYPE] [f_make_Setoid:{dom:Type}{eq1:dom->dom->Prop} C_Setoid (make_Setoid dom eq1)][dom:Type][eq1:dom->dom->Prop] Setoid_elim C_Setoid f_make_Setoid (make_Setoid dom eq1) ==> f_make_Setoid dom eq1] dom = ... : Setoid->Type eq1 = ... : {z:Setoid}(dom z)->(dom z)->Prop Setoid_eq = ... : {S|Setoid}(dom S)->(dom S)->Prop