Commit 2022-01-18 03:54 813a191d

chore(logic/basic): Make higher forall_congr/exists_congr lemmas dependent (#11490) Currently, forall₂_congr and friends take as arguments non dependent propositions like p q : α → β → Prop. This prevents them being useful virtually anywhere as most often foralls are nested like ∀ a, a ∈ s → ... and a ∈ s depends on a. This PR turns them into Π a, β a → Prop (and similar for higher arities). As a bonus, it adds the 5-ary version and golfs all occurrences of nested forall_congrs.