proposition: Lemma filter_aux_transp : Reflexive eq -> transpose_neqkey (Equiv eq) filter_aux.
proof: Proof. unfold transpose_neqkey. intros heq k k' x x' b n. unfold filter_aux. destruct (f k x); destruct (f k' x'); try refl. apply add_transp_Equiv; hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)