proposition: Lemma uniq : forall v:(vect 0), v=vnil.
proof: Proof. intros v. change (v = (eq_rect O vect vnil O (refl_equal O))). generalize (refl_equal O). change ((fun (n : nat) (v : vect n) => forall e : 0 = n, v = eq_rect _ vect vnil _ e) 0 v) in |- * . case v; [intros e |]. - apply K_dec_Type with (p := e). + exact eq_nat_dec. + reflexivity. - discriminate e. Qed.
imports: Arith