proposition: Lemma try_add_arc_irrefl : eq_midex A -> forall x y, transitive R -> irreflexive R -> irreflexive (clos_trans (try_add_arc x y)).
proof: Proof. do 7 intro. apply H1 with x0. destruct (clos_trans_path H2). apply trans_bpath_try_add_arc with x y (length x1); try hyp. apply bp_intro with x1; trivial. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)