```
(def-quasi-constructor pair
"lambda(a:ind_1,b:ind_2,
lambda(x:ind_1,y:ind_2, if(a=x and b=y, an%individual, ?unit%sort)))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor pair?
"lambda(p:sets[ind_1,ind_2], forsome(x:ind_1,y:ind_2, p=pair(x,y)))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor first
"lambda(p:sets[ind_1,ind_2], iota(x:ind_1,forsome(y:ind_2, p=pair(x,y))))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor second
"lambda(p:sets[ind_1,ind_2], iota(y:ind_2,forsome(x:ind_1, p=pair(x,y))))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor i-cross-product
"lambda(a:sets[ind_1],b:sets[ind_2],
indic(p:sets[ind_1,ind_2], pair_q{p} and (first{p} in a) and (second{p} in b)))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-theorem pairs-are-pairs
"forall(x:ind_1,y:ind_2, pair_q(pair(x,y)))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-inference
(instantiate-existential ("x" "y"))
)))
```

```
(def-theorem pairs-are-pairs-rewrite
"forall(x:ind_1,y:ind_2, pair_q(pair(x,y)) iff truth)"
(theory pure-generic-theory-2)
(usages transportable-rewrite)
(proof
(
(apply-macete-with-minor-premises pairs-are-pairs)
)))
```

```
(def-theorem uniqueness-for-pairs
"forall(x_1,x_2:ind_1,y_1,y_2:ind_2,
pair(x_1,y_1) = pair(x_2,y_2) iff (x_1 = x_2 and y_1 = y_2))"
(theory pure-generic-theory-2)
(usages transportable-macete transportable-rewrite)
(proof
(
direct-inference
direct-inference
(block
(script-comment "`direct-inference' at (0)")
(contrapose "with(p:prop,p);")
extensionality
(instantiate-existential ("x_1" "y_1"))
simplify
(antecedent-inference "with(p:prop,p);")
simplify
simplify)
simplify
)))
```

```
(def-theorem reverse-pairs
"forall(x_1,x_2:ind_1,y_1,y_2:ind_2,
pair(x_1,y_1) = pair(x_2,y_2) iff pair(y_1,x_1) = pair(y_2,x_2))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%uniqueness-for-pairs)
direct-and-antecedent-inference-strategy
)))
```

```
(def-theorem first-defined-entails-pair
"forall(p:sets[ind_1,ind_2], #(first(p)) implies pair_q(p))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop, p)")
(eliminate-iota 0)
direct-and-antecedent-inference-strategy
(instantiate-existential ("y%iota"))
(instantiate-existential ("y"))
(contrapose "with(p:prop, forall(x:ind_1,y:ind_2,p))")
(backchain "with(a,b:sets[ind_1,ind_2], a=b)")
(apply-macete-with-minor-premises pairs-are-pairs)
)))
```

```
(def-theorem second-defined-entails-pair
"forall(p:sets[ind_1,ind_2], #(second(p)) implies pair_q(p))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop, p)")
(eliminate-iota 0)
direct-and-antecedent-inference-strategy
(instantiate-existential ("y%iota"))
(instantiate-existential ("x"))
(contrapose "with(p:prop, forall(x:ind_1,y:ind_2,p))")
(backchain "with(a,b:sets[ind_1,ind_2], a=b)")
(apply-macete-with-minor-premises pairs-are-pairs)
)))
```

```
(def-theorem first-projection
"forall(x:ind_1,y:ind_2, first(pair(x,y)) = x)"
(theory pure-generic-theory-2)
(usages transportable-macete transportable-rewrite simplify-logically-first)
(proof
(
direct-inference
(eliminate-iota 0)
(instantiate-existential ("x"))
(instantiate-existential ("y"))
(antecedent-inference-strategy (0 1))
(incorporate-antecedent "with(p:prop, p)")
(incorporate-antecedent "with(p:prop, p)")
(apply-macete-with-minor-premises uniqueness-for-pairs)
simplify
)))
```

```
(def-theorem second-projection
"forall(x:ind_1,y:ind_2, second(pair(x,y)) = y)"
(theory pure-generic-theory-2)
(usages transportable-macete transportable-rewrite simplify-logically-first)
(proof; uses first-projection
(
direct-inference
(disable-quasi-constructor second)
(apply-macete-with-minor-premises reverse-pairs)
(enable-quasi-constructor second)
(apply-macete-with-minor-premises tr%first-projection)
)))
```

```
(def-theorem pair-first-second
"forall(x:sets[ind_1,ind_2],
pair_q(x) implies (pair(first(x),second(x)) = x))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(backchain-repeatedly ("with(p:prop, p)"))
(apply-macete-with-minor-premises first-projection)
(apply-macete-with-minor-premises second-projection)
)))
```

```
(def-theorem pair-first-second-rewrite
"forall(x:sets[ind_1,ind_2],
(pair(first(x),second(x))
= if(pair_q(x),x,lambda(y:ind_1, z:ind_2, ?unit%sort))))"
(theory pure-generic-theory-2)
(usages transportable-rewrite simplify-logically-first)
(proof
(
direct-inference
(case-split ("pair_q{x}"))
(apply-macete-with-minor-premises pair-first-second)
simplify
extensionality
direct-inference
simplify
direct-inference
(eliminate-iota 0)
direct-and-antecedent-inference-strategy
(instantiate-existential ("y%iota"))
auto-instantiate-existential
(contrapose "with(p:prop,not(p))")
(weaken (0 1 2 4))
(backchain "with(p:prop,p)")
(apply-macete-with-minor-premises pairs-are-pairs)
)))
```

```
(def-theorem first-of-a-pair-is-defined
"forall(x:sets[ind_1,ind_2], pair_q(x) implies #(first(x)))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,p)")
(apply-macete-with-minor-premises first-projection)
)))
```

```
(def-theorem second-of-a-pair-is-defined
"forall(x:sets[ind_1,ind_2], pair_q(x) implies #(second(x)))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,p)")
(apply-macete-with-minor-premises second-projection)
)))
```

```
(def-theorem alternate-uniqueness-for-pairs
"forall(x,y:sets[ind_1,ind_2],
(pair_q(x) and pair_q(y))
implies
x=y iff (first(x) = first(y) and second(x) = second(y)))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(weaken (1))
simplify
(apply-macete-with-minor-premises first-of-a-pair-is-defined)
(instantiate-existential ("x_\$0" "y_\$0"))
(weaken (1 2))
simplify
(apply-macete-with-minor-premises second-of-a-pair-is-defined)
(incorporate-antecedent "with(y,x:sets[ind_1,ind_2],first{x}=first{y})")
(incorporate-antecedent "with(y,x:sets[ind_1,ind_2],second{x}=second{y})")
(backchain-repeatedly
("with(y_\$0:ind_2,x_\$0:ind_1,x:sets[ind_1,ind_2], x=pair{x_\$0,y_\$0})"))
(backchain-repeatedly
("with(y_\$2:ind_2,x_\$2:ind_1,y:sets[ind_1,ind_2], y=pair{x_\$2,y_\$2})"))
(apply-macete-with-minor-premises first-projection)
(apply-macete-with-minor-premises second-projection)
(apply-macete-with-minor-premises uniqueness-for-pairs)
direct-and-antecedent-inference-strategy
)))
```

```
(def-compound-macete rewrite-rules-for-pairs
(series
(repeat
tr%pairs-are-pairs
tr%first-projection
tr%second-projection
tr%pair-first-second)
simplify))
```