Commit 2020-07-15 09:51 503a40aa

feat(logic/basic) forall_imp (#3391) Added a missing lemma, which is the one-way implication version of forall_congr.