proposition: Lemma clos_trans_restricted_pair_bis : forall R x y, is_restricted R (x::y::nil) -> clos_trans R y x -> R y x.
proof: Proof. intros. induction H0. hyp. destruct (restricted_clos_trans H H0_). destruct H1. rewrite H1 in H. rewrite H1. tauto. destruct H1. rewrite H1 in H. rewrite H1. tauto. contr. Qed.
imports: CoLoR(ListShrink RelUtil ListUtil LogicUtil)