proposition: Lemma sn_clos_vaeq_intro : forall n (us : Tes n), Vforall (SN R_aeq) us -> SN (clos_vaeq R) us.
proof: Proof. intros n x hx. cut (SN (Vrel1 R_aeq) x). 2: apply Vforall_SN_rel1; hyp. induction 1. apply SN_intro. intros y [x' [xx' [y' [x'y' y'y]]]]. destruct (Vrel1_app_impl x'y') as [i [x'i [a' [j [x'j [k0 [b' [ex' [ey' a'b']]]]]]]]]. gen (Vbreak_eq_app_cast k0 x). set (k0' := Logic.eq_sym k0). set (p := Vbreak (Vcast x k0')). gen (VSn_eq (snd p)). intro e. rewrite e. set (xi := fst p). set (a := Vhead (snd p)). set (xj := Vtail (snd p)). intro ex. clear e. gen (Vbreak_eq_app_cast k0 y). fold k0'. set (q := Vbreak (Vcast y k0')). gen (VSn_eq (snd q)). intro e. rewrite e. set (yi := fst q). set (b := Vhead (snd q)). set (yj := Vtail (snd q)). intro ey. clear e. assert (l : i<n). lia. assert (aa' : a ~~ a'). assert (s1 : a = Vnth x l). rewrite ex, Vnth_cast, Vnth_app. destruct (Compare_dec.le_gt_dec i i). 2: lia. rewrite Vnth_cons_head. refl. lia. assert (s2 : a' = Vnth x' l). rewrite ex', Vnth_cast, Vnth_app. destruct (Compare_dec.le_gt_dec i i). 2: lia. rewrite Vnth_cons_head. refl. lia. rewrite s1, s2. apply Vforall2_elim_nth. hyp. assert (bb' : b ~~ b'). assert (t1 : b = Vnth y l). rewrite ey, Vnth_cast, Vnth_app. destruct (Compare_dec.le_gt_dec i i). 2: lia. rewrite Vnth_cons_head. refl. lia. assert (t2 : b' = Vnth y' l). rewrite ey', Vnth_cast, Vnth_app. destruct (Compare_dec.le_gt_dec i i). 2: lia. rewrite Vnth_cons_head. refl. lia. rewrite t1, t2. apply Vforall2_elim_nth. hyp. assert (h : y ~~~ Vcast (Vapp xi (Vcons b xj)) k0). rewrite ex, ex', Vforall2_cast in xx'. rewrite ey, ey', Vforall2_cast in y'y. trans (Vcast (Vapp x'i (Vcons b x'j)) k0). apply Vforall2_intro_nth. intros k hk. rewrite ey, 2!Vnth_cast, 2!Vnth_app. destruct (Compare_dec.le_gt_dec i k). rewrite 2!Vnth_cons. destruct (NatUtil.lt_ge_dec 0 (k-i)). 2: refl. apply Vforall2_elim_nth. eapply Vforall2_cons_elim. eapply Vforall2_app_elim_r. sym. apply y'y. apply Vforall2_elim_nth. eapply Vforall2_app_elim_l. sym. apply y'y. apply Vforall2_intro_nth. intros k hk. rewrite 2!Vnth_cast, 2!Vnth_app. destruct (Compare_dec.le_gt_dec i k). rewrite 2!Vnth_cons. destruct (NatUtil.lt_ge_dec 0 (k-i)). 2: refl. apply Vforall2_elim_nth. eapply Vforall2_cons_elim. eapply Vforall2_app_elim_r. sym. apply xx'. apply Vforall2_elim_nth. eapply Vforall2_app_elim_l. sym. apply xx'. assert (r : Vrel1 R_aeq x (Vcast (Vapp xi (Vcons b xj)) k0)). rewrite ex. apply Vrel1_cast_intro. apply Vrel1_app_intro_l. apply Vrel1_cons_intro. left. rewrite aa', bb'. intuition. apply incl_clos_aeq. hyp. rewrite h. apply H0. hyp. apply SN_rel1_forall. apply H. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)