Zulip Chat Archive
Stream: Is there code for X?
Topic: imp_iff_imp_left
Yaël Dillies (Sep 06 2021 at 14:09):
This is me being dumb, but where is that lemma?
lemma imp_iff_imp_left (a b c : Prop) : ((a → b) ↔ (a → c)) ↔ (a → (b ↔ c)) := sorry
Yaël Dillies (Sep 06 2021 at 14:14):
Ahah! forall_congr
Last updated: Dec 20 2023 at 11:08 UTC