Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/annoying.v

Created May 27, 2025 14:59
Show Gist options
  • Save EduardoRFS/7fe31feda521f63afae061aee5c1378e to your computer and use it in GitHub Desktop.
Save EduardoRFS/7fe31feda521f63afae061aee5c1378e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
annoying.v
Inductive D : bool -> Type :=
| c0 : D true
| c1 : D false.
Lemma prove_me_general b : forall (v : D b),
v = match b with | true => c0 | false => c1 end.
Proof.
intros v.
induction v; reflexivity.
Qed.
Lemma prove_me : forall (v : D true), v = c0.
Proof.
apply prove_me_general.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment