`{Funext} `{Closeness A} `{forall e x y, IsHProp (close e x y)} : forall x y : Approximation A, approximate _ x = approximate _ y -> x = y. Proof. intros [x Ex] [y Ey];simpl;intros E. destruct E. apply ap. apply path_ishprop. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.