Я не могу точно сказать, что означает результат, который вы пытаетесь доказать, но nil_cons, вероятно, не тот путь.Эта лемма позволяет вам получить False, когда вы уже установили, что [] = a :: l.С другой стороны, ваша цель состоит в том, чтобы вы доказали [] = a :: l, предполагая другой набор гипотез.