Function lemma_permute3_spec_parse_ref 

pub proof fn lemma_permute3_spec_parse_ref<A: SpecParser, B: SpecParser, C: SpecParser>(
    a: A,
    b: B,
    c: C,
)

ensures

forall |ibuf: Seq<u8>| {
    #[trigger] super::Permute3(&a, &b, &c).spec_parse(ibuf)
        == super::Permute3(a, b, c).spec_parse(ibuf)
},

Permute3 denotes the same parser whether its components are owned or borrowed.