proposition: Lemma intersection_dec A (R S : rel A) (Rdec : rel_dec R) (Sdec : rel_dec S) : rel_dec (intersection R S).
proof: Proof. intros x y. unfold intersection. case (Rdec x y); case (Sdec x y); intuition. Defined.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)