proposition: Lemma dec_lem : forall R' R'' x y l, rel_dec R' -> rel_dec R'' -> {z : A | In z l /\ R' x z /\ R'' z y} + {~exists z : A, In z l /\ R' x z /\ R'' z y}.
proof: Proof. induction l; intros. simpl. constructor 2. intro. destruct H. tauto. destruct IHl; try hyp. constructor. destruct s. exists x0. simpl. tauto. destruct (X x a). destruct (X0 a y). constructor. exists a. simpl. tauto. constructor 2. intro. destruct H. simpl in H. decompose [and or] H. rewrite H2 in n0. tauto. assert (exists z : A, In z l /\ R' x z /\ R'' z y). exists x0. tauto. contr. constructor 2. intro. destruct H. simpl in H. decompose [and or] H. rewrite H2 in n0. contr. assert (exists z : A, In z l /\ R' x z /\ R'' z y). exists x0. tauto. contr. Qed.
imports: Coq(Relations List Arith) CoLoR(Path RelMidex RelSub LogicUtil)