The analogue of the eta reduction \x:tau. fx > f eta in dynamic logic would be the equivalence [p?]q = q This is unsound in dynamic logic. Why should it be sound in a typed lambda calculus? -v