Library CoLoR.Util.Relation.NotSN

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-08-08
properties of ~SN terms (using classical logic)

Set Implicit Arguments.


Section S.

  Variables (A : Type) (R : relation A) (x : A) (h : ~SN R x).

  Lemma notSN_succ : exists y, R x y /\ ~SN R y.

End S.