A dependent `forall_const`?

Stream: lean4

[Jovan Gerbscheid]

I ran into the issue that the simp lemma

theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b

is non-dependent, so it didn't apply to my dependent forall. Should the definition be changed to be about an actual forall?

[Aaron Liu]

How can it be both dependent and constant?

[Jovan Gerbscheid]

Ah sorry, in my case the α was equal to True.

[Aaron Liu]

So like docs#forall_true_left

[Jovan Gerbscheid]

Ah, thank you, I didn't have mathlib imported and thought this sort of thing would be in core lean

[Eric Wieser]

There might be a version for Inhabited where the RHS is b default

[Aaron Liu]

docs#Unique.forall_iff