proposition: Lemma sub_rel_try_add_arc_one_to_many : forall x l, R << (try_add_arc_one_to_many x l).
proof: Proof. induction l; simpl; intros. refl. trans (try_add_arc_one_to_many x l). hyp. trans (try_add_arc (try_add_arc_one_to_many x l) x a). apply sub_rel_try_add_arc. apply incl_tc. refl. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)