proposition: Lemma normalise_vars : forall p c c', Elim.normalise c = Some c' -> is_var_of_clause p c <-> is_var_of_clause p c'.
proof: Proof. induction c;simpl. - intros. inv H. tauto. - intros. destruct (Elim.normalise c) eqn: N; try discriminate. destruct (Elim.get_polarity_rec (var a) c0) eqn: G. destruct p0. destruct (eq_dec (make (negb b) (var a)) a); try discriminate. inv H. rewrite is_var_of_clause_cons. apply make_var in n. rewrite negb_involutive in n. rewrite IHc by auto. assert (G' : Elim.get_polarity_rec (var a) c' <> None) by congruence. apply get_polarity_spec_var in G'. intuition congruence. inv H. rewrite! is_var_of_clause_cons. rewrite IHc by auto. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause