Skip to content

Instantly share code, notes, and snippets.

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 koba-e964/4492d43e941e2016a9eae750d2e8adc7 to your computer and use it in GitHub Desktop.
Save koba-e964/4492d43e941e2016a9eae750d2e8adc7 to your computer and use it in GitHub Desktop.
universe u
constant t: Sort u
constant f: t -> t
constant x: t
lemma test: x = x := by reflexivity
lemma test2: f.{u u} x.{u} = f.{u u} x.{u} := by reflexivity
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment