proposition: Lemma Vforall2_app_elim_r n1 (v1 : vector A n1) (v1' : vector B n1) n2 (v2 : vector A n2) (v2' : vector B n2) : Vforall2 (Vapp v1 v2) (Vapp v1' v2') -> Vforall2 v2 v2'.
proof: Proof. intro h. apply Vforall2_intro_nth. intros i hi. assert (hi' : n1+i < n1+n2). lia. assert (a1 : Vnth v2 hi = Vnth (Vapp v1 v2) hi'). rewrite Vnth_app. destruct (Compare_dec.le_gt_dec n1 (n1+i)). apply Vnth_eq. lia. lia. assert (a2 : Vnth v2' hi = Vnth (Vapp v1' v2') hi'). rewrite Vnth_app. destruct (Compare_dec.le_gt_dec n1 (n1+i)). apply Vnth_eq. lia. lia. rewrite a1, a2. apply Vforall2_elim_nth. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)