proposition: Lemma clos_vaeq_cons : forall u v n (us vs : Tes n), Vcons u us ==>R Vcons v vs <-> (u =>R v /\ us ~~~ vs) \/ (u ~~ v /\ us ==>R vs).
proof: Proof. intros u v n us vs. split. intros [x [uusx [y [xy yvvs]]]]. revert uusx yvvs xy. VSntac x. VSntac y. rewrite !Vforall2_cons_eq. intros [h1 h2] [i1 i2] h. inversion h. left. subst x0 y0 x'. rewrite h1, <- i1, h2, H5, i2. split. apply incl_clos_aeq. hyp. refl. right. subst x0 y0 y'. rewrite h1, H4, i1. split. refl. ex (Vtail x). intuition. ex (Vtail y). intuition. intros [[h1 h2]|[h1 h2]]. inversion h1; subst. ex (Vcons u' us). split. rewrite Vforall2_cons_eq. intuition. ex (Vcons v' us). split. apply Vrel1_cons_intro. auto. rewrite Vforall2_cons_eq. intuition. destruct h2 as [us' [usus' [vs' [us'vs' vs'vs]]]]. ex (Vcons v us'). rewrite Vforall2_cons_eq. intuition. ex (Vcons v vs'). rewrite Vforall2_cons_eq. intuition. apply Vrel1_cons_intro. right. intuition. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)