CODE:

// 0
// 自然数の先頭元を表す
struct zero
{
	typedef zero eval;
};

// 任意の自然数 N の successor s(N)
// N の次の自然数を表す
template 
struct suc
{
	typedef suc eval;
};

// 任意の自然数 N, M に対して、加算 N + M を定義する
// テンプレートの特殊化により分岐
template 
struct add
{
	typedef typename add::eval eval;
};

// N + 0 = N
template 
struct add
{
	typedef typename N::eval eval;
};

// N + s(M) = s(N + M)
template 
struct add>
{
	typedef typename suc>::eval eval;
};

// 1 := s(0), 2 := s(1) = s(s(0)) と定義する
// 1 + 1 = 2を証明する
int main()
{
	// 左辺 1 + 1
	add, suc>::eval lhs;
	
	// 右辺 2
	suc>::eval rhs;

	// コンパイルが通れば証明完了
	lhs = rhs;
}