search

Ayertienna / IS5

Intuitionistic S5 logic formalization
4 stars 0 forks source link

ok_LF is preserved under permutation #40

Closed Ayertienna closed 11 years ago

Ayertienna commented 11 years ago

forall X (G: list (var * X)) G', G = G' -> forall U, ok_LF G U <-> ok_LF G' U

This seems obvious, but the definition of permutation (from tlc) is causing headaches again...

Ayertienna commented 11 years ago

Done