proposition: Lemma sn_red_sn : forall a b : term, sn a -> red a b -> sn b.
proof: Proof. unfold sn in |- *. simple induction 2; intros; auto with coc core arith sets. apply Acc_inv with P; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations