proposition: Lemma RU (C C' : clause) : R (C `|` C') = (R C `|` R C').
proof: Proof. by rewrite /R sepU fimsetU. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)