proposition: Lemma try_add_arc_many_to_many_midex : eq_midex A -> forall l l', incl l' l -> is_restricted R l -> rel_midex R -> rel_midex (try_add_arc_many_to_many l' l).
proof: Proof. induction l'; simpl; intros. hyp. pose (incl_cons_l_incl H0). apply try_add_arc_one_to_many_midex with l. hyp. apply H0. simpl. tauto. refl. apply restricted_try_add_arc_many_to_many; hyp. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)