proposition: Lemma try_add_arc_one_to_many_irrefl : eq_midex A -> forall x l l', is_restricted R l -> transitive R -> irreflexive R -> irreflexive (try_add_arc_one_to_many x l').
proof: Proof. induction l'; simpl; intros. hyp. apply try_add_arc_irrefl. hyp. destruct l'; simpl. hyp. apply tc_trans. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)