proposition: Lemma has_form_of_literal : forall m l, has_literal m l <-> has_form m (form_of_literal l).
proof: Proof. destruct l ; simpl in *; tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause