proposition: Lemma extensionnality2 : forall a b, a <> b -> (exists i, select a i <> select b i).
proof: Proof. intros. apply not_all_ex_not. unfold not in *. intros. apply H. apply extensionnality; auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance Classical_Pred_Type ClassicalEpsilon