proposition: Lemma try_add_arc_sym : forall x y z t, try_add_arc x y z t -> try_add_arc x y t z -> R z t.
proof: Proof. intros. inversion H. hyp. inversion H0. contr. rewrite H3 in H7. contr. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)