Skip to content

Instantly share code, notes, and snippets.

@BekaValentine

BekaValentine/gist:88d6d21e31312cd06a0cc4801ca48322

Created August 29, 2016 18:14
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save BekaValentine/88d6d21e31312cd06a0cc4801ca48322 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save BekaValentine/88d6d21e31312cd06a0cc4801ca48322 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
("!- \p. (snd p, fst p) : A*B -> B*A"
"->I"
("p : A*B !- (snd p, fst p) : B*A"
"*I"
("p : A*B !- snd p : B"
"*E2"
("p : A*B !- p : A*B"
"hyp"))
("p : A*B !- fst p : A"
"*E1"
("p : A*B !- p : A*B"
"hyp")))
@BekaValentine

BekaValentine commented Aug 29, 2016 •
edited
Loading

Copy link
Copy Markdown
Author 
!- \p. (snd p, fst p) : A*B -> B*A     by ->I

    p : A*B !- (snd p, fst p) : B*A     by *I

        p : A*B !- snd p : B     by *E2

            p : A*B !- p : A*B     by hyp

        p : A*B !- fst p : A     by *E1

            p : A*B !- p : A*B    by hyp

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment