proposition: Lemma equal_more_IfEq : forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l, IfEq (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> IfEq (equal_more cmp x1 d1 cont (More x2 d2 r2 e2)) ((x1,d1)::l) (flatten_e (More x2 d2 r2 e2)).
proof: Proof. unfold IfEq; simpl; intros; destruct X.compare; simpl; auto. rewrite <-andb_lazy_alt; f_equal; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int