Function lemma_permute4_spec_parse_ref 

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

ensures

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

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