proposition: Lemma match_option_dec : forall p o, match_option p o \/ ~ match_option p o.
proof: Proof. destruct o; simpl. destruct (hformula_eq_dec p h);tauto. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause