proposition: Lemma lex_SN_eq : forall a b, SN lex (a,b) -> forall a', eqA a a' -> SN lex (a',b).
proof: Proof. intros a b SN_ab a' eqaa'. inversion SN_ab. apply SN_intro. destruct y as (a'',b'). intro H'. inversion H'; subst a'0 b'0 a0 b0; apply H. apply lex1. apply (incl_elim Hcomp). exists a'. auto. apply lex2. apply (eqA_trans eqaa' H3). exact H5. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)