coq: Tactic to replace true hypothesis in 'and' statement

Question

Assumptions:
l: a < d

Goal: (s a /\ a < d) <-> s a

Here, I have an /\ with an assumed statement. The goal just needs l to be applied, but I cant seem to figure out the tactic. Apply, rewrite, and replace don't work.

Answer 1

I figured it out -- you just have to run propositional, which will evaluate such tautological logic automatically.