Technique for proving lower bounds on NFAs