proposition: Lemma equal_B2P: forall (m m' : farray), equal m m' = true <-> equalP m m'.
proof: Proof. intros. split; intros. apply equal_eq in H. rewrite H. unfold equalP. now rewrite equal_refl. apply equal_eqP in H. now rewrite H, equal_refl. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses ProofIrrelevance