ink

theorem Mt.Utils.forall_ext {α : Type} {f : α → Prop} {g : α → Prop} (h : ∀ (a : α), f a = g a) : ((a : α) → f a) = ((a : α) → g a)