proposition: Lemma Equal_Equivb : forall (m m':farray), Equal m m' <-> Equivb m m'.
proof: Proof. intros; rewrite Equal_Equiv. apply Equiv_Equivb; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses