proposition: Lemma cons_IfEq : forall b x1 x2 d1 d2 l1 l2, X.eq x1 x2 -> cmp d1 d2 = true -> IfEq b l1 l2 -> IfEq b ((x1,d1)::l1) ((x2,d2)::l2).
proof: Proof. unfold IfEq; destruct b; simpl; intros; destruct X.compare; simpl; try rewrite H0; auto; order. Qed.
imports: FunInd FMapInterface FMapList ZArith Int