Prove assumed properties of permut, ok_Bg & emptyEquiv

Ayertienna / IS5

Intuitionistic S5 logic formalization

4 stars 0 forks source link

Closed Ayertienna closed 12 years ago

Ayertienna commented 12 years ago

The properties seem trivial, but they require proofs nevertheless.

Ayertienna commented 12 years ago

Duplicate for #6, #7 -- this will be part of automation