This commit is contained in:
Ellen Arvidsson 2025-06-27 02:45:56 +02:00
parent bc9d138960
commit 65066c493e

View file

@ -116,7 +116,7 @@ n fresh
// 1 + n! premises // 1 + n! premises
// trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion // trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion
c, γ* ⊢ a_1, ..., a_n c, γ* ⊢ a_1, ..., a_n, δ*
∀ I ⊆ {1, ..., n}. ∀ I ⊆ {1, ..., n}.
c, γ* ⊢ { a_i | i ∈ I }, δ* c, γ* ⊢ { a_i | i ∈ I }, δ*
OR OR