Q_close_symm@{} : forall e, Symmetric (@close Q _ e). Proof. red;unfold close;simpl. intros e x y [E1 E2];split. - apply flip_lt_negate. rewrite <-negate_swap_r,involutive. trivial. - apply flip_lt_negate. rewrite negate_swap_r,involutive. trivial. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.