Require Import Bvector. Fixpoint constVec (A : Set) (a : A) (n : nat) : vector A n := match n return vector A n with | 0 => Vnil A | S n' => Vcons A a n' (constVec A a n') end. Hypothesis (A : Prop). Definition myProp (b : bool) : Prop := if b then A -> A else A. Goal myProp true. intro a. assumption. Qed. Fixpoint doubleVec (A : Set) (n : nat) (v : vector A n) : vector A (n + n) := match v in vector _ n return vector A (n + n) with | Vnil => Vnil A | Vcons a n' v' => eq_rect (S (S n' + n')) (vector A) (Vcons A a (S (n' + n')) (Vcons A a (n' + n') (doubleVec A n' v'))) (S n' + S n') (plus_n_Sm (S n') n') end. Definition doubleVec' : forall (X : Set) (n : nat) (v : vector X n), vector X (n + n). intros X n v. induction v. constructor. simpl. constructor. exact a. cut (n + S n = S (n + n)). intro. rewrite H. constructor. exact a. exact IHv. apply sym_eq. apply plus_n_Sm. Defined. Print doubleVec'. Definition addition : nat -> nat -> nat. intros. assumption. Defined. Extraction doubleVec.