-
- and の introduction
env |- A env |- B
---------------------
env |- A ∧ B
- and の elimination
A ∧ B という仮定が A と B という 2 つの仮定に分かれる。
env |- A -> B -> P
--------------------
env |- A ∧ B -> P
- or の introduction
env |- A
---------------
env |- A ∨ B
env |- B
---------------
env |- A ∨ B
- or の elimination
env |- A -> P env |- B -> P
-------------------------------
env |- A ∨ B -> P
- exists の introduction
Q[t/x]
-------------------------------
env, t : A |- exists x : A, Q
- exists の elimination
すべての x について成り立つのなら，特定の x についても成り立つ。
env |- P x -> P0
-------------------
env |- ex P -> P0
- apply ... with ～.
... の部分を～で置き換えたものを適用する。
(例) 仮定のほうに変数として A を含む H があったとして，
apply H with (A := fun x : nat => x).
