proposition: Lemma xror_clause_clause : forall a f, fst (xror_clause_cnf a f) = xor_clause_cnf a f.
proof: Proof. unfold xror_clause_cnf. unfold xor_clause_cnf. assert (ACC: fst (@nil clause, null) = nil) by reflexivity. intros a f. set (F1:= (fun '(acc, tg) (e : clause) => match ror_clause a e with | inl cl => (cl :: acc, tg) | inr l => (acc, merge tg l) end)). set (F2:= (fun (acc : list clause) (e : clause) => match or_clause a e with | Some cl => cl :: acc | None => acc end)). revert ACC. generalize (@nil clause, null). generalize (@nil clause). induction f as [|a0 f IHf]; simpl ; auto. intros ? p ?. apply IHf. unfold F1 , F2. destruct p ; simpl in * ; subst. clear. revert a0. induction a as [|a a0 IHa]; simpl; auto. intros a1. destruct (radd_term a a1) eqn:RADD. - apply radd_term_term in RADD. rewrite RADD. auto. - destruct (add_term a a1) eqn:RADD'. + apply radd_term_term' in RADD'. congruence. + reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid