Added separation algebras for finite functions and sum types.

Added bi-logics for views in preparation for Jonas' defence.