proposition: Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2, X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2).
proof: Proof. destruct c; simpl; intros; MX.elim_comp; auto with ordered_type. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia