proposition: Lemma midex_lem : forall R' R'' x y l, rel_midex R' -> rel_midex R'' -> (exists 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 H1. tauto. destruct IHl; try hyp. constructor. destruct H1. exists x0. simpl. tauto. destruct (H x a). destruct (H0 a y). constructor. exists a. simpl. tauto. constructor 2. intro. destruct H4. simpl in H4. decompose [and or] H4. rewrite H7 in H3. tauto. assert (exists z : A, In z l /\ R' x z /\ R'' z y). exists x0. tauto. contr. constructor 2. intro. destruct H3. simpl in H3. decompose [and or] H3. rewrite H6 in H2. 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)