proposition: Lemma extensionality2 : forall a b, a <> b -> exists i, select a i <> select b i.
proof: Proof. intros a b Hab. destruct (diff_index_p Hab) as [i Hi]. now exists i. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance