class zero {};
template<typename N> class succ {};
template<typename N, typename M> class add {};






template<typename N, typename M>
class eq
{
private:
   eq() {}
   friend class axiom;
};

class axiom
{
public:
   template<typename X>
      static eq<X, X> reflexive() { return eq<X, X>(); }

   template<typename X, typename Y>
      static eq<X, Y> symmetric( eq<Y, X> ) { return eq<X, Y>(); }

   template<typename X, typename Y, typename Z>
      static eq<X, Z> transitive( eq<X, Y>, eq<Y, Z> ) { return eq<X, Z>(); }

   template<typename X, typename Y>
      static eq< succ<X>, succ<Y> > suc( eq<X, Y> ) { return eq< succ<X>, succ<Y> >(); }

   template<typename Y>
      static eq< add<zero,Y>, Y > zero_plus() { return eq< add<zero,Y>, Y >(); }

   template<typename X, typename Y>
      static eq< add<succ<X>,Y>, succ< add<X,Y> > > succ_plus()
         { return eq< add<succ<X>,Y>, succ< add<X,Y> > >(); }
};






template<typename T, typename X, typename V>
	struct replace {
		typedef T type;
	};
template<typename X, typename V>
	struct replace<X,X,V> {
		typedef V type;
	};
template<template<class,class> class Bin, typename T1, typename T2, typename X, typename V>
	struct replace<Bin<T1,T2>,X,V> {
		typedef Bin<typename replace<T1,X,V>::type,
		            typename replace<T2,X,V>::type> type;
	};

template<typename T>
	struct fresh {
		typedef fresh type;
	};







template<typename X, typename PROP>
class forall
{
private:
   forall() {}
   typedef typename fresh<PROP>::type N;
public:
   forall(
      typename replace< PROP, X, zero >::type,
      typename replace< PROP, X, succ<N> >::type (*)( typename replace<PROP, X, N>::type )
   ) {}
};






eq< add<zero,zero>, add<zero,zero> > case_zero()
{
   return axiom::reflexive< add<zero,zero> >();
}

template<typename N>
   eq< add<succ<N>,zero>, add<zero,succ<N> > > case_step( eq< add<N,zero>, add<zero,N> > indhyp )
   {
      eq<         add<zero,N> , N                   > p1 = axiom::zero_plus<N>();
      eq<         add<N,zero> , N                   > p2 = axiom::transitive( indhyp, p1 );
      eq< succ< add<N,zero> > , succ<N>             > p3 = axiom::suc( p2 );
      eq<   add<succ<N>,zero> , succ< add<N,zero> > > p4 = axiom::succ_plus<N,zero>();
      eq<   add<succ<N>,zero> , succ<N>             > p5 = axiom::transitive( p4, p3 );
      eq< add< zero,succ<N> > , succ<N>             > p6 = axiom::zero_plus< succ<N> >();
      eq<             succ<N> , add< zero,succ<N> > > p7 = axiom::symmetric( p6 );
      eq<   add<succ<N>,zero> , add< zero,succ<N> > > p8 = axiom::transitive( p5, p7 );
      return p8;
   }







class X {};

int main()
{
   // 1+1 = 2
   {
      eq< add< succ<zero>, succ<zero> >, succ< add< zero, succ<zero> > > > p1
         = axiom::succ_plus< zero, succ<zero> >();

      eq< add< zero, succ<zero> >, succ<zero> > p2
         = axiom::zero_plus< succ<zero> >();

      eq< succ< add< zero, succ<zero> > >, succ< succ<zero> > > p3
         = axiom::suc( p2 );

      eq< add< succ<zero>, succ<zero> >, succ< succ<zero> > > proof_of_1_plus_1_is_2
         = axiom::transitive( p1, p3 );
   }

   // forall X. X+0=0+X
   {
      forall< X, eq< add<X,zero>, add<zero,X> > > proof( case_zero(), &case_step );
   }
}