pub fn data_processing_inequality_ty() -> Expr
Data processing inequality: I(X;Z) ≤ I(X;Y) for Markov chain X→Y→Z Type: Prop