simp only [SimpleEdges_adj, hab, not_false_eq_true, true_and, ne_eq, not_forall, not_not] at hab'
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
hab' : ¬SimpleEdges.Adj a b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
hab' : ∃ x, sbtw a x b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b