checkpoint some tidbits for a more computable rep invariant for Inode
checkpoint some tidbits for a more computable rep invariant for Inode

perhaps this will avoid the need for manual instantiation (currently
Haogang has a clever trick for manual instantiation -- sticking the
new shape of the representation into the postcondition as an extra
lifted Prop).

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl