proposition: Lemma units_has_literal_add : forall m l u l' (WF : wf_map u) (HF : Annot.lift (has_literal m) l) , units_has_literal m (add_literal l u) l' -> units_has_literal m u l' \/ l = l'.
proof: Proof. unfold units_has_literal. intros. destruct H. unfold add_literal in *. rewrite gsspec in H by auto. destruct (eqs (Annot.lift id_of_literal l') (id_of_literal (Annot.elt l))). - inv H. right. unfold Annot.lift in *. destruct l,l'. simpl in *. subst. f_equal. unfold id_of_literal in *. destruct elt1; destruct elt0 ; simpl in *; try congruence; f_equal. apply has_form_eq with (m:=m) ;auto. apply has_form_eq with (m:=m) ;auto. - left ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause