proposition: Theorem append_splitVector: forall (A : Set) n1 n2 (x : Vector.t A (n1 + n2)) x1 x2, (x1, x2) = (splitVector n1 n2 x) -> (Vector.append x1 x2) = x.
proof: Proof. intuition. specialize (append_splitVector_h _ _ x); intuition. rewrite <- H in H0. simpl in *. trivial. Qed.
imports: FCF.FCF FCF.SemEquiv FCF.DetSem