look at k-prelude.k. In the translation of these rules, you will find the use of [ KList ]

you can find these examples in k-prelude.kore

for example:
  rule heat({ redex(K:K):K => .KList }
 , _:KList , heated(_:KList , { .KList => K:K }
):K):K [ owise,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((233,3,234,11)), kore]

rule { '_[_/_](M:Map ,  [ .KList ]  ,  [ .KList ] ):Map => M:Map }