proposition: Lemma Vrel1_cons_elim : forall x1 x2 n (v1 v2 : vector A n), Vrel1 R (Vcons x1 v1) (Vcons x2 v2) -> (R x1 x2 /\ v1 = v2) \/ (x1 = x2 /\ Vrel1 R v1 v2).
proof: Proof. intros. simpl in H. unfold Vhead_tail in H. simpl in H. inversion H; auto. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)