Hi. I got a couple of types like this:
Inductive foo : Type := | Foo. Inductive fooDenote : list nat -> Type := | FooDenote: fooDenote nil.
Is it possible to prove this goal?
Goal fooDenote (cons 3 nil) -> False. Proof.
I mean, there is no constructor which can make
foo  true as it mentions only the case for
Goal fooDenote (cons 3 nil) -> False. Proof. intros H; inversion H. Qed.
Last updated: Oct 04 2023 at 23:01 UTC