proposition: Lemma tr_sn : forall E v V, E |- v ~: V -> SN R_aeq v.
proof: Proof. intros E v V ht. eapply int_sn. rewrite <- subs_id. eapply tr_int. apply ht. apply valid_id. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)