some small changes
sketch iso. proofs (Duality.hs)