proposition: Lemma eLcmp_fstmap l1 l2 f : (forall k k', E.compare (f k) (f k') = E.compare k k') -> eLcmp (List.map (fstmap f) l1) (List.map (fstmap f) l2) = eLcmp l1 l2.
proof: Proof. revert l2. induction l1 as [|(x1,d1) l1 IH]; destruct l2 as [|(x2,d2) l2]; intros E; simpl; auto. rewrite E. case E.compare_spec; try easy. unfold E.eq. intros <-. destruct (cmp d1 d2); auto. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)