Function lemma_utc_time_encode_wf 

pub proof fn lemma_utc_time_encode_wf<const DER: bool>(value: UtcTime)

requires

value.wf(),

DER ==> value.precision == TimePrecision::Second,

ensures

utc_time_bytes_wf::<DER>(utc_time_bytes(value)),

utc_time_value(utc_time_bytes(value)) == Some(value),