proposition: Lemma clos_vaeq_sub : forall n (us vs : Tes n) p q (h : p+q<=n), us ==>R vs -> Vsub us h ~~~ Vsub vs h \/ Vsub us h ==>R Vsub vs h.
proof: Proof. intros n us vs p q h [us' [usus' [vs' [r vsvs']]]]; symmetry in vsvs'. destruct (Vrel1_sub h r). left. rewrite (Vforall2_sub h usus'), (Vforall2_sub h vsvs'), H. refl. right. ex (Vsub us' h). split. apply Vforall2_sub. hyp. ex (Vsub vs' h). split. hyp. apply Vforall2_sub. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)