// proof4 : succ(succ(zero)) = succ(zero) + succ(zero) let proof4 : Eq<Succ<Succ<Zero>>,Add<Succ<Zero>, Succ<Zero>>> = transitive(s:Add<Succ<Zero>,Succ<Zero>>.self,t: Succ<Add<Succ<Zero>, Zero>>.self,r: Succ<Succ<Zero>>.self)(proof1)(proof3)

(edited)

7:08 AM

うまく、ハイライトでけた。この辺りとか、わりと推論できないのかね?

7:10 AM

// proof4 : succ(succ(zero)) = succ(zero) + succ(zero) let proof4 : Eq<Succ<Succ<Zero>>,Add<Succ<Zero>, Succ<Zero>>> = transitive(proof1)(proof3)

7:10 AM

こんな感じにしたさがある。