Alternative ways to write defineContents

In File System Lesson I, we needed to express the fact that a directory is the parent of its contents. The following facts are all equivalent ways of expressing that constraint.

fact { all d: Dir, o: d.contents | o.parent = d }

fact { all d: Dir | all o: d.contents | o.parent = d }

fact { all d: Dir, o: FSObject | o in d.contents => o.parent = d }

fact { all d: Dir | all o: FSObject | o in d.contents => o.parent = d }