Let p and q be given.
Assume Hp: p ∈ EuclidPlane.
Assume Hq: q ∈ EuclidPlane.
We will prove apply_fun EuclidPlane_metric (p,q) = distance_R2 p q.
We prove the intermediate claim Hpq: (p,q) ∈ (setprod EuclidPlane EuclidPlane).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma EuclidPlane EuclidPlane p q Hp Hq).
rewrite the current goal using (apply_fun_graph (setprod EuclidPlane EuclidPlane) (λpq0 : set ⇒ distance_R2 (pq0 0) (pq0 1)) (p,q) Hpq) (from left to right).
rewrite the current goal using (tuple_2_0_eq p q) (from left to right).
rewrite the current goal using (tuple_2_1_eq p q) (from left to right).
Use reflexivity.
∎