proposition: Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2.
proof: Proof. intros f1; induction f1 as [|a f1 IHf1] ; simpl ; auto. intros f2. specialize (IHf1 f2). destruct(ror_cnf f1 f2). rewrite <- ror_clause_clause. destruct(ror_clause_cnf a f2). simpl. rewrite <- IHf1. reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid