proposition: Lemma SN_compat : forall a, SN gtA a -> forall a', eqA a a' -> SN gtA a'.
proof: Proof. intros a SN_a a' eqaa'. apply SN_intro. intros a'' gta'a''. inversion SN_a. apply H. apply (incl_elim Hcomp). exists a'. auto. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)