A relational logic primerΒΆ

Note

A question of style!

all x,y : Dir, e : Entry | x->e in entries and y->e in entries implies x=y
all e : Entry | lone entries.e
entries.~entries in iden