Function lemma_and_then_spec_parse_congruence 

pub proof fn lemma_and_then_spec_parse_congruence<Tail1: SpecParser<PVal = Seq<u8>>, Tail2: SpecParser<PVal = Seq<u8>>, Then1: SpecParser, Then2: SpecParser<PVal = Then1::PVal>>(
    tail1: Tail1,
    tail2: Tail2,
    then1: Then1,
    then2: Then2,
)

requires

forall |x: Seq<u8>| #[trigger] tail1.spec_parse(x) == tail2.spec_parse(x),

forall |x: Seq<u8>| #[trigger] then1.spec_parse(x) == then2.spec_parse(x),

ensures

forall |x: Seq<u8>| {
    #[trigger] AndThen(tail1, then1).spec_parse(x) == AndThen(tail2, then2).spec_parse(x)
},