proposition: Lemma list_compare_sym : forall x y, list_compare y x = CompOpp (list_compare x y).
proof: Proof. induction x; destruct y; simpl;auto. rewrite uint_compare_sym. destruct (id a ?= id h); simpl;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause