proposition: Lemma SN_st_lam x u : SN R (Lam x u) -> SN R u.
proof: Proof. intro h. eapply SN_st. apply h. apply st_lam. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)