8af80418ba1ec431c8027fa9668e5678658d3611Allan Fostervar a

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterpred phi : a

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster. (forall x: a . phi x) = ((\ x: a . phi x) =e= \ x: a . ())

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fostervar p : Logical

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster. p \/ not p

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster