Function lemma_serializer_congruent_reflexive 

pub broadcast proof fn lemma_serializer_congruent_reflexive<A>(a: A)
where
    A: Consistency + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,

ensures

#[trigger] serializer_congruent(a, a),