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