proposition: Lemma eq_hc_trans : forall {A:Type} [x y r:HCons.t A], HCons.eq_hc x r = true -> eq_hc y r = true -> HCons.eq_hc x y = true.
proof: Proof. intros. unfold eq_hc in *. rewrite andb_true_iff in *. rewrite Bool.eqb_true_iff in *. destruct H; destruct H0 ; intuition try congruence. lia. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause