proposition: Lemma try_add_arc_midex : eq_midex A -> forall x y, rel_midex R -> rel_midex (try_add_arc x y).
proof: Proof. do 6 intro. destruct (H0 x0 y0). do 2 constructor. hyp. destruct (H x0 y0). constructor 2. intro. inversion H3; contr. destruct (H0 y0 x0). constructor 2. intro. inversion H4; contr. destruct (H x x0). destruct (H y y0). rewrite H4, H5. constructor. constructor 2; hyp. constructor 2. intro. inversion H6; contr. constructor 2. intro. inversion H5; contr. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)