proposition: Lemma SN_notNT_eq : forall x, SN R x <-> ~NT R x.
proof: Proof. intro x. split. apply SN_notNT. apply contraposee. intro h. cut (NT R x). fo. revert h. apply notSN_NT. Qed.
imports: CoLoR(DepChoice NotSN SN RelUtil LogicUtil ClassicUtil)