proposition: Lemma Vrel1_cons_intro : forall x1 x2 n (v1 v2 : vector A n), (R x1 x2 /\ v1 = v2) \/ (x1 = x2 /\ Vrel1 R v1 v2) -> Vrel1 R (Vcons x1 v1) (Vcons x2 v2).
proof: Proof. intros. simpl. unfold Vhead_tail. simpl. destruct H; destruct H. subst v2. apply left_sym. hyp. subst x2. apply right_sym. hyp. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)