proposition: Lemma ror_clause_clause : forall a f, fst (ror_clause_cnf a f) = or_clause_cnf a f.
proof: Proof. unfold ror_clause_cnf,or_clause_cnf. intros a; destruct a ; auto. apply xror_clause_clause. Qed.
imports: List Refl Bool Relation_Definitions Setoid