Software Foundations

Rel.v

反射推移閉包とかこれ何かの役に立つんじゃろか。関係をラップするとか。

clos_refl_transとかrefl_step_closureとかまったく意図とか分かってないけど、だいたいこんな感じだろうというレバガチャで証明は出来た。

何の役に立つとか、読み進めたら出てくるんだろうか。それまで読むことが出来るだろうか。