proposition: Lemma extensionnality_eqb : forall a b, (forall i, select a i = select b i) -> equal a b = true.
proof: Proof. intros. unfold select in H. cut (a.(default) = b.(default)). intro Hd. 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. rewrite <- Hd. apply a.(nodefault). + apply find_2 in H0. contradict H0. unfold MapsTo. rewrite Hd. apply b.(nodefault). } apply find_ext_dec. split; auto. cut (exists k, find k a = None /\ find k b = None). intro. destruct H0 as (k, (Ha, Hb)). specialize (H k). rewrite Ha, Hb in H. auto. destruct a, b; simpl in *. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance