```
"lambda(f:[pp_0,pp_1],
forsome(a:rr, 0<=a and forall(x,y:pp_0,#(f(x)) and #(f(y)) implies dist_1(f(x),f(y))<=dist_0(x,y)*(a+dist_0(x,y)))))"
(theory metric-spaces-2-tuples))
```

```
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-existential ("min(1,eps/(1+a))"))
(weaken (0))
(unfold-single-defined-constant (0) min)
(case-split ("1<=eps/(1+a)"))
simplify
simplify
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(antecedent-inference "with(a,eps:rr,y_\$0,x_\$0:pp_0,f:[pp_0,pp_1],
#(f(x_\$0))
and
#(f(y_\$0))
and
dist_0(x_\$0,y_\$0)<=min(1,eps/(1+a)));")
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("dist_0(x_\$0,y_\$0)*(a+dist_0(x_\$0,y_\$0))"))
(backchain "with(a:rr,f:[pp_0,pp_1],
forall(x,y:pp_0,
#(f(x)) and #(f(y))
implies
dist_1(f(x),f(y))<=dist_0(x,y)*(a+dist_0(x,y))));")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("(eps/(1+a))*(a+1)"))
(apply-macete-with-minor-premises monotone-product-lemma)
(cut-with-single-formula "min(1,eps/(1+a))<=1 and min(1,eps/(1+a))<=eps/(1+a)")
simplify
(apply-macete-with-minor-premises minimum-2nd-arg)
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(instantiate-universal-antecedent "with(a:rr,f:[pp_0,pp_1],
forall(x,y:pp_0,
#(f(x)) and #(f(y))
implies
dist_1(f(x),f(y))<=dist_0(x,y)*(a+dist_0(x,y))));" ("x_\$0" "y_\$0"))
))

(usages transportable-macete)
(theory metric-spaces-2-tuples))
```