proposition: Theorem splitVector_append : forall (A : Set) n1 (v1 : Vector.t A n1) n2 (v2 : Vector.t A n2), splitVector n1 n2 (Vector.append v1 v2) = (v1, v2).
proof: Proof. induction v1; intuition; simpl in *. remember ( splitVector n n2 (Vector.append v1 v2)) as z. destruct z. rewrite IHv1 in Heqz. inversion Heqz; subst. trivial. Qed.
imports: FCF.FCF FCF.SemEquiv FCF.DetSem