Могу ли я "сопоставить" "OF" со списком лемм

Question

Я только что написал этот код:

lemmas gc_step_intros =
  normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)]
  normal[OF step.intros(4)] normal[OF step.intros(5)] drop

где step.intros на самом деле только 5 лемм. Есть ли удобный способ избежать этого повторения, то есть то, что может выглядеть следующим образом?

lemmas gc_step_intros = normal[OF_EACH step.intros] drop

Answer 1

Ты можешь использовать THEN вместо OF и использовать тот факт, что атрибут применяется ко всем теорем в списке теорем. Следующее должно делать то, что вы хотите:

lemmas gc_step_intros = step.intros[THEN normal] drop