proposition: Lemma Vsub_cons_intro : forall n (v : vector A n) i k (h : i+k<=n) (p : k>0), Vsub v h = Vcast (Vcons (Vnth v (Vsub_cons_intro_aux1 h p)) (Vsub v (Vsub_cons_intro_aux2 h p))) (Vsub_cons_intro_aux3 p).
proof: Proof. intros. apply Vsub_cons_intro_aux. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)