proposition: Lemma add_transp : transpose_neqkey Equal (@add A).
proof: Proof. unfold transpose_neqkey. intros k l x y m n. unfold Equal. intro k'. rewrite !add_o. destruct (eq_dec k k'); destruct (eq_dec l k'); try refl. absurd (E.eq k l). hyp. trans k'; hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)