c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../../propositional/soundness/prop.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundFOL : FOLPF -> FOLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBaseFOL.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundIFOL.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundTND.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder non_empty_universe := existsE non_empty_universe [u][_] (impE exists1 (existsI u (trans beta true1))).