proposition: Lemma sn_clos_vaeq_elim : forall n i (hi : i<n) (us : Tes n), SN (clos_vaeq R) us -> SN R_aeq (Vnth us hi).
proof: Proof. intros n i hi us hus. elim hus; clear us hus. intros us h1 h2. apply SN_intro. intros ui' uiui'. destruct (clos_aeq_inv uiui') as [vi [vi' [uivi [ui'vi' vivi']]]]; clear uiui'. rewrite <- (Vnth_replace hi hi us). apply h2. ex (Vreplace us hi vi). split. apply Vforall2_intro_nth. intros j jn. destruct (eq_nat_dec j i). subst j. rewrite Vnth_replace. rewrite (Vnth_eq _ jn hi); auto. rewrite Vnth_replace_neq. refl. lia. ex (Vreplace us hi vi'). split. rewrite Vrel1_nth_iff. ex i hi. split. rewrite !Vnth_replace. hyp. intros j jn jni. rewrite !Vnth_replace_neq; auto. apply Vforall2_intro_nth. intros j jn. destruct (eq_nat_dec j i). subst j. rewrite !Vnth_replace. hyp. rewrite !Vnth_replace_neq; auto. refl. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)