Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/countable_setoid.v

Created August 4, 2023 11:40
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Blaisorblade/9628895ae8892b87f4d45d96af284f15 to your computer and use it in GitHub Desktop.
Save Blaisorblade/9628895ae8892b87f4d45d96af284f15 to your computer and use it in GitHub Desktop.
Download ZIP
stdpp countable setoids are LeibnizEquiv
Raw
countable_setoid.v
From stdpp Require Import prelude countable ssreflect.
Section test.
Context `{CA : Countable A} `{!Equiv A} `{!Equivalence (≡@{A})}.
Goal Proper (equiv ==> eq) (encode (A := A)) -> LeibnizEquiv A.
Proof. intros HP x y H. apply: (inj encode). by rewrite H. Qed.
End test.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment