Let X, d, x and y be given.

Assume Hm: metric_on X d.

Assume Hx: x ∈ X.

Assume Hy: y ∈ X.

We prove the intermediate claim Hsym: ∀x0 y0 : set, x0 ∈ X → y0 ∈ X → apply_fun d (x0,y0) = apply_fun d (y0,x0).

Apply Hm to the current goal.

Assume Hcore Htri.

Apply Hcore to the current goal.

Assume Hcore2 Hposdef.

Apply Hcore2 to the current goal.

Assume Hab Hrefl.

Apply Hab to the current goal.

Assume Hf Hsym.

An exact proof term for the current goal is Hsym.

An exact proof term for the current goal is (Hsym x y Hx Hy).

∎