Make the conclusion of local contexts W-Ind empty.

The conclusion of W-Ind,
"\WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ}", is changed to
"\WF{E;~\ind{p}{Γ_I}{Γ_C}}{}" because
local contexts should be empty when
inductive definition is defined globally.
This is consistent with W-Global-Assum and W-Global-Def.

The side condition "c_i ∉ Γ ∪ E" which I changed previous commit is
changed again to "c_i ∉  E" because I guess that it tries to
avoid name conflicts to the local contexts in the conclusion.
However, the condition is useless after the local contexts is empty.

0 files changed, 0 insertions, 0 deletions