added further material on lifted equality on type sigma
added Coq proof (from Satallax) for Modal Collapse