proposition: Lemma restricted_try_add_arc_one_to_many : forall l x l', In x l -> incl l' l -> is_restricted R l -> is_restricted (try_add_arc_one_to_many x l') l.
proof: Proof. induction l'; simpl; intros. hyp. apply restricted_clos_trans. apply restricted_try_add_arc. hyp. apply H0. simpl. tauto. apply IHl'. hyp. exact (incl_cons_l_incl H0). hyp. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)