proposition: Lemma eval_literal_same : forall l P, eval_literal_rec l (eval_literal_rec l P) <-> eval_literal_rec l P.
proof: Proof. destruct l ; simpl. tauto. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause