Function lemma_and_then_parser_congruence 

pub broadcast proof fn lemma_and_then_parser_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

parser_congruent(tail1, tail2),

parser_congruent(then1, then2),

ensures

#[trigger] parser_congruent(AndThen(tail1, then1), AndThen(tail2, then2)),