proposition: Lemma extensionality_eqb : forall a b, (forall i, select a i = select b i) -> equal a b = true.
proof: Proof. intros. unfold select in H. assert (forall i, find i a = find i b). - intro i. specialize (H i). case_eq (find i a); case_eq (find i b); intros; rewrite H0 in *; rewrite H1 in *; subst; auto. + apply find_2 in H1. contradict H1. unfold MapsTo. apply a.(nodefault). + apply find_2 in H0. contradict H0. unfold MapsTo. apply b.(nodefault). - apply find_ext_dec in H0. exact H0. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance