proposition: Lemma Vrel1_app_impl : forall n (v1 v2 : vector A n), Vrel1 R v1 v2 -> Vrel1_app R v1 v2.
proof: Proof. induction v1; simpl. intros. contr. intro. VSntac v2. unfold Vhead_tail. simpl. intro. inversion H0. ex 0 (@Vnil A) h n (Vtail v2) (eq_refl (S n)) (Vhead v2). split. refl. split. refl. hyp. ded (IHv1 (Vtail v2) H2). do 8 destruct H6. destruct H7. rewrite H6, H7. ex (S x0) (Vcons (Vhead v2) x1) x2 x3 x4. assert (S x0 + S x3 = S n). lia. ex H9 x6. simpl. rewrite !Vcast_cons, (eq_unique (@eq_add_S (x0 + (S x3)) n H9) x5). intuition. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)