Function declassification_ty 

pub fn declassification_ty() -> Expr

Declassification : Expr → SecurityLabel → SecurityLabel → Prop Explicit declassification from high to low label.