proposition: Lemma sub_rel_try_add_arc_many_to_many : forall l l', R << (try_add_arc_many_to_many l' l).
proof: Proof. induction l'; simpl; intros. refl. trans (try_add_arc_many_to_many l' l). hyp. apply sub_rel_try_add_arc_one_to_many. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)