proposition: Lemma compare_aux_Cmp : forall e, Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)).
proof: Proof. intros e; functional induction (compare_aux e); simpl in *; auto; intros; try clear e0; try clear e3; try MX.elim_comp; auto. rewrite 2 cons_1 in IHc; auto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia