proposition: Lemma Vrel1_app_intro_l : forall n (v : vector A n) m (v1 v2 : vector A m), Vrel1 R v1 v2 -> Vrel1 R (Vapp v v1) (Vapp v v2).
proof: Proof. induction v; intros. hyp. simpl. unfold Vhead_tail. simpl. apply right_sym. apply IHv. hyp. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)