Function systematic_encoding_ty 

pub fn systematic_encoding_ty() -> Expr

systematic_encoding : Nat → Nat → Prop — every linear code is equivalent to a code in systematic form.