proposition: Lemma path_try_add_arc_path : forall t x y l z, ~(x=z \/ In x l) \/ ~(y=t \/ In y l) -> path (try_add_arc x y) z t l -> path R z t l.
proof: Proof. induction l; simpl; intros. inversion H0; tauto. destruct H0. split. inversion H0. hyp. rewrite H5 in H. tauto. apply IHl. pose sym_equal. pose (e A x a). tauto. hyp. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)