証明のテキスト化の準備

導出：

1. false-elim ＝ initial : ⊥ → P
2. true-intro ＝ final : P → T
3. forall-elim ＝ instantiate ＝ projection : ∀x∈X.P(x) → P(a)
4. exists-intro ＝ uninstantiate = injection ： P(a) → ∃x∈X.P(x)

リーズニング：

1. Forall-Intro-Right :: (x∈X. φ(x):A→P(x)) ⇒ (A → ∀x∈X.P(x))
2. Exists-Intro-Left :: (x∈X. φ(x):P(x)→B) ⇒ (∃x∈X.P(x) → B)
3. Imp-Intro :: (A, B → C) ⇒ (A → C<*B)
4. Imp-Elim :: (A → C<*B) ⇒ (A, B → C)
5. Comp :: (Γ → Δ), (Δ → Σ) ⇒ (Γ → Σ)
6. Not-Intro :: (Γ, A → ⊥) ⇒ (Γ → ￢A)
7. Not-Elim :: (Γ → ￢A) ⇒ (Γ , A → ⊥)

ブロック（ボックス）：

キーワード	短縮	意味
sequence	seq	Compの連続
conjunction	conj	Forall-Intro-Right
disjunction	disj	Exists-Intro-Left
implication	imp	Imp-Intro
application	app	Imp-Elim
absurd	abs	Not-Intro
contradict	contr	Not-Elim

テキスト化の例（まだ未定）：

begin implication
  postulate A
  assume B
  ...
  C
end implicatin
Now we have
  A → (C < B)

begin sequence
  postilate ∀x∈X.P(x)
  by instantiate[X, P, a]
  P(a)  --(1)
  by premise P12
  P(a) > B --(2)
  from 1, 2 by MP
  B
end sequence
Now we have ∀x∈X.P(x) → B