proposition: Lemma Vrel1_app_iff : forall n (v1 v2 : vector A n), Vrel1 R v1 v2 <-> Vrel1_app R v1 v2.
proof: Proof. intros n v1 v2. split. apply Vrel1_app_impl. intros [i [vi [x [j [vj [h [y [h1 [h2 h3]]]]]]]]]; subst. rewrite 2!Vcast_refl. apply Vrel1_app_intro_l. apply Vrel1_cons_intro. fo. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)