proposition: Lemma InA_eqke_eqk : forall k1 k2 e1 e2 l, E.eq k1 k2 -> InA eqke (k1,e1) l -> InA eqk (k2,e2) l.
proof: Proof. intros k1 k2 e1 e2 l Hk. rewrite 2 InA_alt. intros ((k',e') & (Hk',He') & H); simpl in *. exists (k',e'); split; auto. red; simpl; eauto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface