pos_eq@{} : forall a b : Q+, @paths Q (' a) (' b) -> a = b. Proof. intros [a Ea] [b Eb] E. change (a = b) in E. destruct E;apply ap;apply path_ishprop. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.