proposition: Lemma add_transp_Equiv : Reflexive eq -> transpose_neqkey (Equiv eq) (@add A).
proof: Proof. intro heq. eapply transpose_neqkey_m'. apply Equal_Equiv. intuition. refl. apply add_transp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)