Skip to content

Instantly share code, notes, and snippets.

@hmaurer

hmaurer/gist:11199034

Forked from BekaValentine/gist:11198998
Created April 23, 2014 00:29
Show Gist options
  • Save hmaurer/11199034 to your computer and use it in GitHub Desktop.
Save hmaurer/11199034 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
... = begin
suc (a + suc b)
==< cong suc (lemma2 a b) >
suc (suc (a + b))
==< cong (suc.suc) (comm a b) >
suc (suc (b + a))
==< cong suc (sym (lemma2 b a)) >
suc (b + suc a)
[]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment