Skip to content

Instantly share code, notes, and snippets.

@roboguy13

roboguy13/Surj.v

Created December 20, 2021 22:00
Show Gist options
  • Save roboguy13/6cb07d0f671c9f5ddef48bb7856e2d05 to your computer and use it in GitHub Desktop.
Save roboguy13/6cb07d0f671c9f5ddef48bb7856e2d05 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Surj.v
Require Import Coq.Logic.FinFun.
Theorem the_theorem
: ~ exists (f : unit -> bool), Surjective f.
Proof.
intro H.
destruct H.
destruct (H true).
destruct (H false).
destruct x0, x1.
rewrite H0 in H1.
discriminate H1.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment