proposition: Lemma restricted_try_add_arc : forall x y l, In x l -> In y l -> is_restricted R l -> is_restricted (try_add_arc x y) l.
proof: Proof. unfold is_restricted. intros. inversion H2. apply H1. hyp. rewrite <- H5, <- H6. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)