proposition: Lemma eqd_inj: forall n m x y, @eqd n m n m x y -> x = y.
proof: Proof. intros. apply Eqdep_dec.eq_dep_eq_dec in H; trivial. decide equality; apply pos_eq_dec. Qed.
imports: ATBR(Common Classes) Coq(FMapPositive) Coq(Eqdep)