proposition: Lemma eval_literal_rec_swap : forall w w' p, eval_literal_rec w (eval_literal_rec w' p) -> eval_literal (neg_literal w') -> (eval_literal_rec w p).
proof: Proof. destruct w,w' ; simpl; try tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause