Давайте подумаем о чем-то подобном Section
в качестве примера
Section myList.
Variable X : Type.
Definition myListApp2 (l1 l2 : list X) :=
app l1 l2.
Definition myListApp3 (l1 l2 l3 : list X) :=
app (app l1 l2) l3.
Definition NoXUse n := S n.
Definition myListApp4 (l1 l2 l3 l4 : list X) :=
app (app (app l1 l2) l3) l4.
End myList.
Arguments myListApp2 {X}.
Arguments myListApp3 {X}.
Arguments myListApp4 {X}.
после End
из Section
Мне нужно установить первый аргумент всех определений, неявных вручную, есть ли Любой способ сказать Coq, что Variable X
всегда неявно?