proposition: Lemma for_all_aux_transp : transpose_neqkey Logic.eq for_all_aux.
proof: Proof. unfold transpose_neqkey. intros k k' x x' b n. unfold for_all_aux. bool. rewrite andb_comm with (b1:=f k x). refl. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)