fact: Definition vector_double_rect : forall (A:Type) (X: forall (n:nat), t A n -> t A n -> Type), X 0 nil nil -> (forall n (v1 v2 : t A n) a b, X n v1 v2 -> X (S n) (cons a v1) (cons b v2)) -> forall n (v1 v2 : t A n), X n v1 v2.
imports: Bool Arith Vector