proposition: Lemma extensionnality : forall a b, (forall i, select a i = select b i) -> equal a b = true.
proof: Proof. intros. unfold select in H. apply find_ext_dec in H. exact H. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses