proposition: Lemma restriction_midex : eq_midex A -> rel_midex R -> rel_midex restriction.
proof: Proof. unfold restriction. do 4 intro. destruct (H0 x y). destruct (In_midex H x l). destruct (In_midex H y l). constructor. tauto. constructor 2. tauto. constructor 2. tauto. constructor 2. tauto. Qed.
imports: CoLoR(ListShrink RelUtil ListUtil LogicUtil)