[[children]] kind = "lemma" path = "lemmas/子引理"