Commit 2019-07-22 01:35 f24dc98b

feat(logic/unique): forall_iff and exists_iff (#1249) Maybe these should be @[simp]. My use case in fin 1 and it's slightly annoying to have default (fin 1) everwhere instead of 0, but maybe that should also be a @[simp] lemma.