proposition: Lemma Equal_trans : forall (elt:Type)(m m' m'' : t elt), Equal m m' -> Equal m' m'' -> Equal m m''.
proof: Proof. unfold Equal; congruence. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface