proposition: Lemma try_add_arc_dec : eq_dec A -> forall x y, rel_dec R -> rel_dec (try_add_arc x y).
proof: Proof. repeat intro. destruct (X0 x0 y0). do 2 constructor. hyp. destruct (X x0 y0). constructor 2. intro. inversion H; contr. destruct (X0 y0 x0). constructor 2. intro. inversion H; contr. destruct (X x x0). destruct (X y y0). rewrite e, e0. constructor. constructor 2; hyp. constructor 2. intro. inversion H; contr. constructor 2. intro. inversion H; contr. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)