proposition: Lemma Vin_elim : forall x n (v : vector A n), Vin x v -> exists n1 (v1 : vector A n1) n2 (v2 : vector A n2) (H : n1 + S n2 = n), v = Vcast (Vapp v1 (Vcons x v2)) H.
proof: Proof. induction v; simpl. contr. intro H. destruct H. clear IHv. subst x. ex 0 (@Vnil A) n. ex v (eq_refl (S n)). rewrite Vcast_refl. refl. assert (exists n1 (v1 : vector A n1) n2 (v2 : vector A n2) (H : n1 + S n2 = n), v = Vcast (Vapp v1 (Vcons x v2)) H). exact (IHv H). destruct H0 as [n1]. destruct H0 as [v1]. destruct H0 as [n2]. destruct H0 as [v2]. destruct H0 as [H1]. exists (S n1). exists (Vcons h v1). exists n2. exists v2. exists (S_add_S H1). rewrite H0. clear H0. simpl. generalize (S_add_S H1); intros i; inversion i as [j]. rewrite Vcast_cons. f_equal. apply Vcast_pi. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)