Are not rules applied in succession?

I am trying this:

makeless[x_, y_] := {
  Imp[x, y] -> True,
  Imp[And[p___, x, q___], y] -> True
  }

myrules = {
   Imp[x_, True] -> True,
   And[p___, Imp[x_, y_], q___] :> 
      And[And @@ ({p} //. makeless[x, y]), Imp[x, y], And @@ ({q} //. makeless[x, y])]
   };

(need to implement intuitionistic implication).

I expect

Imp[a, True] && b //. myrules

to return b, but it just returns the same (i. e. Imp[a, True] && b).

Should not the first rule in the list, Imp[x_, True] -> True be applied first? It would then give True && b which would evaluate to b.

What am I doing wrong and how to do it right?