Function captured_any_contents 

pub open spec fn captured_any_contents(children: Seq<Captured<AnySpec>>) -> Seq<u8>

{ children.map(|_i: int, child: Captured<AnySpec>| child.encoded).flatten() }