proposition: Lemma Bvector_ne_exists : forall (n : nat)(v : Bvector n), n > 0 -> exists v', v <> v'.
proof: Proof. induction n; intuition. lia. destruct (vector_S v). destruct H0. exists (Vector.cons bool (negb x) n x0). intuition. rewrite H0 in H1. inversion H1. destruct x; simpl in *; discriminate. Qed.
imports: FCF.FCF Permutation