{-
OPLSS 22 : Introduction to Type Theory
Tuesday Exercises

Try to prove the following propositions.
Warning: not all of them may be provable!

C-c C-l load
\<=> ⇔
\and ∧
...
\neg ¬

In the shed.
C- C-, see goal and givens
C-c C-, like C-c C-. but also shows the type of your partial solution.
C-c C-SPC  check solution, and remove shed
C-c C-r    refine, use function or do lambdas
C-c C-c    pattern matching (if you give a parameter) or copatternmatching (no par).
-}
open import mylib

p1 : P ⇔ P ∧ P
p1 = {!!}

p2 : P ∨ ¬ P ⇒ (¬ (P ∧ Q) ⇔ ¬ P ∨ ¬ Q)
p2 = {!!}

p3 : ¬ (P ∧ ¬ P)
p3 = {!!}

p4 : ¬ (P ⇔ ¬ P)
p4 = {!!}

p5 : ¬ ¬ (P ∨ ¬ P)
p5 = {!!}

p6 : ¬ P ⇔ ¬ ¬ ¬ P
p6 = {!!}

p7 : (¬ ¬ P ⇒ P) ⇒ (P ∨ ¬ P)
p7 = {!!}

p8 : (P ∨ ¬ P) ⇒ ¬ ¬ P ⇒ P
p8 = {!!}