proposition: Lemma notWF_EIS_eq : ~WF R <-> EIS R.
proof: Proof. rewrite WF_notIS_eq, not_forall_eq. intuition; destruct H as [f hf]; exists f. apply NNPP. hyp. auto. Qed.
imports: CoLoR(DepChoice NotSN SN RelUtil LogicUtil ClassicUtil)