Этот вопрос касается проекта, которым я занимаюсь, а именно кодирования Principia Mathematica на Coq. Principia разработал правила вывода, одним из которых является Syll: ∀ P Q R: Опора, P → Q, Q → R: P → R Я пытаюсь создать сценарий Ltac,...