// proof1 : succ(zero) + succ(zero) = succ(zero + succ(zero)) // use axiom3 let proof1 : Eq<Add<Succ<Zero>,Succ<Zero>>, Succ<Add<Succ<Zero>,Zero>>> = axiom3() // proof2 : succ(zero) + zero = succ(zero) let proof2 : Eq<Add<Succ<Zero>, Zero>, Succ<Zero>> = axiom2() // proof3 : succ( succ(zero) + zero ) = succ(succ(zero)) let proof3 : Eq<Succ<Add<Succ<Zero>, Zero>>,Succ<Succ<Zero>>> = axiom1()(proof2) // proof4 : succ(succ(zero)) = succ(zero) + succ(zero) let proof4 : Eq<Succ<Succ<Zero>>,Add<Succ<Zero>, Succ<Zero>>> = transitive()(proof1)(proof3) // proof5 : succ(zero) + succ(zero) = succ(succ(zero)) let proof5 : Eq<Add<Succ<Zero>, Succ<Zero>>,Succ<Succ<Zero>>> = symmetric()(proof4)