proposition: Lemma has_literal_eq: forall m x y (HX: has_literal m x) (HY: has_literal m y) (EQ : (eq_literal x y) = true), x = y.
proof: Proof. unfold eq_literal. intros. destruct x as [f|f]; destruct f; destruct y; try congruence. f_equal. eapply has_form_eq; eauto. simpl in *. lia. f_equal. eapply has_form_eq; eauto. simpl in *. lia. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause