student here, just started learning Coq. I'm essentially trying to prove that [] = a::l where (a:A) and (l: list A) is False, solving all subgoals. I found a nifty Coq Library function called nil_cons but I get an error when trying to apply it. Does anyone have any advice? Thanks in advance!
I can't tell exactly what the result you're trying to prove means, but nil_cons is probably not the way to go. That lemma allows you to derive False when you have already established that [] = a :: l. Your goal, on the other hand, wants you to prove [] = a :: l assuming a different set of hypotheses.
