added some more lines and useful things

nngcheatsheet.org

@@ -14,3 +14,11 @@
  + =intro h= lets you take a goal of the form =A -> B= and turn it into a goal of =B= with the assumption =h : A=. This is, basically, *function definition* and you're declaring an argument named =h= with type =A= and you get to use that =h= in the "body" of your "function" when making your proof
    + You can actually do multiple =intro= on one line like =intro h1 h2 h3= in order to take a goal of =A -> B -> C -> D= and turn it into a goal of =D= with the assumptions =h1 : A=, =h2 : B=, =h3 : C=, &c.
      + Pop-quiz! If I have a goal of type =(A -> B) -> C= what is the type of =h= if I do =intro h=?
+ + =use= lets you prove an existential goal by providing an example of a thing that fits the condition
+ + =cases= lets you take apart an existential assumption and get back *a* thing that satisfies the proposition. You don't get to know *what* it is specifically, just that it is *a* thing
+   + =cases= is also useful when you need to take a hypothesis of =false= and end the proof. Why does this work? Well, remember how in classical logic =F -> q= evaluates to true no matter what =q= is? 
+* Strategies
+ + Don't use induction until after you've taken stock of what theorems might apply to the situation. If you look and don't see something that could obviously apply, then you probably need induction.
+ + If a proof isn't immediately obvious, try sketching it out with pen and paper instead
+ + When proving an existential goal, think hard about what you need
+   + Again, try writing it out