proposition: Lemma Vrel1_cast_elim : forall m n (h : m=n) (v1 v2 : vector A m), Vrel1 R (Vcast v1 h) (Vcast v2 h) -> Vrel1 R v1 v2.
proof: Proof. induction m; destruct n; intros. assert (h = eq_refl 0). apply eq_unique. subst h. contr. discr. discr. assert (v1 = Vcons (Vhead v1) (Vtail v1)). apply VSn_eq. rewrite H0. assert (v2 = Vcons (Vhead v2) (Vtail v2)). apply VSn_eq. rewrite H1. rewrite H0, H1, !Vcast_cons in H. simpl in H. unfold Vhead_tail in H. simpl in H. apply Vrel1_cons_intro. inversion H. left. split. hyp. eapply Vcast_eq_elim with (m := n). apply H6. right. split. refl. eapply IHm with (n := n). apply H3. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)