Function real_fmt 

pub open spec fn real_fmt<const DER: bool>() -> RealInnerFmt

{ Refined(Tail, |bytes: Seq<u8>| real_bytes_wf::<DER>(bytes)) }