proposition: Lemma list_compare_trans : forall (c : comparison) x y z, list_compare x y = c -> list_compare y z = c -> list_compare x z = c.
proof: Proof. induction x; destruct y; destruct z; simpl; try congruence; auto. destruct (id a ?= id h) eqn:IDA ; destruct (id h ?= id h0) eqn:IDH ; destruct (id a ?= id h0) eqn:IDH0 ; repeat Lib.elim_compare; try lia; try congruence. eapply IHx;eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause