proposition: Lemma Vrel1_add_intro : forall x1 x2 n (v1 v2 : vector A n), (R x1 x2 /\ v1 = v2) \/ (x1 = x2 /\ Vrel1 R v1 v2) -> Vrel1 R (Vadd v1 x1) (Vadd v2 x2).
proof: Proof. intros x1 x2. induction n; intros v1 v2. VOtac. intuition. apply left_sym. hyp. VSntac v1; VSntac v2. simpl Vadd. intros [[h1 h2]|[h1 h2]]. Veqtac. apply Vrel1_cons_intro. right. fo. subst x2. destruct (Vrel1_cons_elim h2) as [[i1 i2]|[i1 i2]]. rewrite i2. apply Vrel1_cons_intro. left. fo. apply Vrel1_cons_intro. right. fo. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)