proposition: Lemma has_literal_mono : isMono has_literal.
proof: Proof. unfold isMono. intros. destruct x ; simpl in *. eapply has_form_mono;eauto. eapply has_form_mono;eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause