(n +2)度目：カリー／ハワード対応

And_intro	And intro
And_left	And elim left
And_right	And elim right
Or_inl	Or intro left
Or_inr	Or intro right
fun_OR_MAKE	なぜか無い
後で定義	Or elim
特殊	Imp intro
MP（不要だが）	Imp elim
trivial	True intro
EFQ	False elim
不要	Not intro
後で定義	Not elim

• MP = modus ponens
• EFQ = ex falso quodlibet エクス・ファルソ・クァドリベット

メタ関数の関数化：

• fun_IMP_INTRO = id
• fun_NOT_INTRO
• fun_AND_INTRO

関数	定理・証明
関数のデータ化	定理・証明の命題化
メタ関数	メタ定理・証明＝リーズニング
メタ関数の関数化	リーズニングの定理化

実際に必要なもの：

1. And
   1. And_intro
   2. And_left
   3. And_right
2. Or
   1. Or_inl
   2. Or_inr
   3. fun_OR_MAKE
3. True
   1. trivial
4. False
   1. EFQ