Function lemma_fn_prepare_specs 

pub proof fn lemma_fn_prepare_specs<T, Spec, Exec>(
    prepare: &FnPrepare<T, Spec, Exec>,
    value: T::V,
)
where
    T: DeepView + ?Sized,
    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
    Exec: Fn(&T) -> Result<usize, PreSerializeError>,

ensures

prepare.consistent(value) == prepare.spec_fn@.consistent(value),

prepare.byte_len(value) == prepare.spec_fn@.byte_len(value),

Exposes the consistency and byte-length specification bundled into an FnPrepare.