proposition: Lemma sn_wn `{!∀ y, Decision (red R y)} x : sn R x → wn R x.
proof: Proof. induction 1 as [x _ IH]. destruct (decide (red R x)) as [[x' ?]|?]. - destruct (IH x') as (y&?&?); eauto using wn_step. - by apply nf_wn. Qed.
imports: stdpp(options)