```(def-language relational-language
(base-types uu)
(constants
(equiv "[uu,uu,prop]"0)))
```

```
(def-theory relational-theory
(language relational-language)
(component-theories h-o-real-arithmetic)
(axioms
(equiv-transitivity
"forall(a,b,c:uu, a equiv b and b equiv c implies a equiv c)")
(equiv-reflexivity
"forall(a:uu, a equiv a)")
(equiv-symmetry
"forall(a,b:uu, a equiv b implies b equiv a)")))
```

```
(def-constant equiv%class
"lambda(x:uu, indic{y:uu, x equiv y})"
(theory relational-theory))

```

```
(def-constant equiv%class_q
"lambda(a:sets[uu], forsome(y:uu, a=equiv%class(y)))"
(theory relational-theory))
```

```(def-theorem ()
"forsome(a:sets[uu], equiv%class_q(a))"
(theory relational-theory)
(proof
(
(instantiate-existential ("with(x:uu,equiv%class(x))"))
unfold-defined-constants
unfold-defined-constants
(instantiate-existential ("x"))
unfold-defined-constants
)))
```

```
(def-atomic-sort uu_q
"equiv%class_q"
(theory relational-theory))

```

```(def-theory-ensemble relational-theory)
```

```(def-theory-ensemble-multiple relational-theory 2)
```

```(def-theory-ensemble-overloadings metric-spaces (1))
```

```(def-overloading equiv
(relational-theory equiv)
(relational-theory-2-tuples equiv_0)
(relational-theory-2-tuples equiv_1))
```

```
(def-constant equiv%on%classes%unary
"lambda(f:[uu_0,uu_1], forall(a,b:uu_0, a equiv b implies f(a) equiv f(b)))"
(theory relational-theory-2-tuples))
```