Q_triangular@{} : Triangular Q. Proof. hnf. intros u v w e d E1 E2. apply Q_triangular_one with v. - symmetry;trivial. - trivial. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.