Exercises
Video examples
- Commutativity: A, B; A && B |- B && A
Easy
- Introduction: A, B; |- A -> (B -> (A && B))
- Left elimination: A, B; |- A && B -> A
- Right elimination: A, B; |- A && B -> B
Medium
- Currying: A, B, C; (A && B) -> C |- A -> (B -> C)
- Uncurrying: A, B, C; A -> (B -> C) |- (A && B) -> C
- Weak distributivity of ∧ over ⇒: A, B, C; (A -> B) && C |- A -> (B && C)
Advanced
- Associativity: A, B, C; |- (A && (B && C)) <-> ((A && B) && C)
- Distributivity of ⇒ over ∧: A, B, C; |- (A -> (B && C)) <-> ((A -> B) && (A -> C))