diff --git a/Example.lean b/Example.lean
index 03155d3..99b94d2 100644
--- a/Example.lean
+++ b/Example.lean
@@ -1,4 +1,159 @@
-import Aesop
+variable (p q r : Prop)
 
-def main : IO Unit :=
-  IO.println "Cirno's Perfect Arithmetics Class has begun!"
+-- commutativity of ∧ and ∨
+example : p ∧ q ↔ q ∧ p := by
+  apply Iff.intro
+  · intro pandq
+    apply And.intro
+    · apply And.right pandq
+    · apply And.left pandq
+  · intro qandp
+    apply And.intro
+    · apply And.right qandp
+    · apply And.left qandp
+
+example : p ∨ q ↔ q ∨ p := by
+  apply Iff.intro
+  · intro porq
+    cases porq with
+    | inl p => exact Or.inr p
+    | inr q => exact Or.inl q
+  · intro qorp
+    cases qorp with
+    | inl q => exact Or.inr q
+    | inr p => exact Or.inl p
+
+-- associativity of ∧ and ∨
+example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := by
+  apply Iff.intro
+  · intro pqandr
+    apply And.intro
+    · exact And.left (And.left pqandr)
+    · apply And.intro
+      · exact And.right (And.left pqandr)
+      · exact And.right pqandr
+  · intro pandqr
+    apply And.intro
+    · apply And.intro
+      · exact And.left pandqr
+      · exact And.left (And.right pandqr)
+    ·  exact And.right (And.right pandqr)
+
+example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
+  apply Iff.intro
+  · intro pqorr
+    cases pqorr with
+    | inr r => apply Or.inr (Or.inr r)
+    | inl porq => cases porq with
+      | inl p => apply Or.inl p
+      | inr q => apply Or.inr (Or.inl q)
+  · intro porqr
+    cases porqr with
+    | inl p => apply Or.inl (Or.inl p)
+    | inr qorr => cases qorr with
+      | inr r => apply Or.inr r
+      | inl q => apply Or.inl (Or.inr q)
+
+-- distributivity
+example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
+  apply Iff.intro
+  · intro pandqorr
+    cases pandqorr with
+    | intro p qor => cases qor with
+      | inl q => apply Or.inl (And.intro p q)
+      | inr r => apply Or.inr (And.intro p r)
+  · intro pandqorpandr
+    cases pandqorpandr with
+    | inl pandq => apply And.intro (And.left pandq) (Or.inl (And.right pandq))
+    | inr pandr => apply And.intro (And.left pandr) (Or.inr (And.right pandr))
+
+example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by
+  apply Iff.intro
+  · intro porqandr
+    cases porqandr with
+    | inl p => apply And.intro (Or.inl p) (Or.inl p)
+    | inr qandr => apply And.intro (Or.inr (And.left qandr)) (Or.inr (And.right qandr))
+  · intro porqandporr
+    cases And.left porqandporr with
+    | inl p => apply Or.inl p
+    | inr q => cases And.right porqandporr with
+      | inl p => apply Or.inl p
+      | inr r => apply Or.inr (And.intro q r)
+
+-- other properties
+example : (p → (q → r)) ↔ (p ∧ q → r) := by
+  apply Iff.intro
+  · intro ptoqtor
+    intro pandq
+    exact ptoqtor (And.left pandq) (And.right pandq)
+  · intro pandqtor
+    intro p
+    intro q
+    exact pandqtor (And.intro p q)
+
+example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := by
+  apply Iff.intro
+  · intro porqtor
+    apply And.intro
+    · intro p
+      exact porqtor (Or.inl p)
+    · intro q
+      exact porqtor (Or.inr q)
+  · intro ptorandqtor
+    intro porq
+    cases porq with
+    | inl p => exact (And.left ptorandqtor) p
+    | inr q => exact (And.right ptorandqtor) q
+
+example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by
+  apply Iff.intro
+  · intro nporq
+    apply And.intro
+    · intro p
+      exact nporq (Or.inl p)
+    · intro q
+      exact nporq (Or.inr q)
+  · intro npandnq
+    intro porq
+    cases porq with
+    | inl p => exact (And.left npandnq) p
+    | inr q => exact (And.right npandnq) q
+
+example : ¬p ∨ ¬q → ¬(p ∧ q) := by
+  intro npornq
+  cases npornq with
+  | inl np => intro pandq; exact np (And.left pandq)
+  | inr nq => intro pandq; exact nq (And.right pandq)
+
+example : ¬(p ∧ ¬p) := by
+  intro pandnp
+  exact (And.right pandnp) (And.left pandnp)
+
+example : p ∧ ¬q → ¬(p → q) :=
+  λ ⟨p,nq⟩ ptoq => nq (ptoq p)
+
+example : ¬p → (p → q) :=
+  λ np p => absurd p np
+
+example : (¬p ∨ q) → (p → q)
+  | (Or.inl np), p => absurd p np
+  | (Or.inr q), _ => q
+
+example : p ∨ False ↔ p := by
+  apply Iff.intro
+  · intro porf
+    apply Or.elim porf id False.elim
+  · intro p
+    apply Or.inl p
+
+
+example : p ∧ False ↔ False := by
+  apply Iff.intro
+  · intro ⟨p,f⟩
+    exact f
+  · intro f
+    apply False.elim f
+
+
+example : (p → q) → (¬q → ¬p) :=
+ λ ptoq nq p => absurd (ptoq p) nq