proposition: Lemma WF_notIS_eq : WF R <-> forall f, ~IS R f.
proof: Proof. split. intros wf f hf. ded (wf (f 0)). rewrite SN_notNT_eq in H. apply H. exists f. auto. intros h x. rewrite SN_notNT_eq. intros [f [h0 hf]]. eapply h. apply hf. Qed.
imports: CoLoR(DepChoice NotSN SN RelUtil LogicUtil ClassicUtil)