More cases for completeness

[Ailrun]

Related: #87

Context, substitution, and variable cases are all done.
Now it's only natural number cases (which are most tedious and complex...)

However, I realized that the natural number cases requires a "stronger" functionality of eval (i.e. functionality modulo equivalence of environment), so I decided to make a separate PR after this.

[Ailrun]

However, I realized that the natural number cases requires a "stronger" functionality of eval (i.e. functionality modulo equivalence of environment), so I decided to make a separate PR after this.

Actually, this stronger functionality is not true (because of the Π a p B case which contains p). Maybe we need to bring functional extensionality again here to compare ps.

[Ailrun]

Or we can define a weaker notion of equality between two domain values so that it compares that kind of environment occurence in a pointwise manner.

[HuStmpHrrr]

where do we need to compare environments? I don't think we need that in Agda

[HuStmpHrrr]

Or we can define a weaker notion of equality between two domain values so that it compares that kind of environment occurence in a pointwise manner.

I wouldn't say this is a good idea. This will make the model tremendously difficult to work with.

[Ailrun]

Now I think about it, maybe they are definitionally equal. The target was drop_env (p \mapsto a \mapsto b) and p \mapsto a if I remember correctly. (I hope it's not the other way around, i.e. dropping first and adding the top member)

[HuStmpHrrr]

Now I think about it, maybe they are definitionally equal. The target was drop_env (p \mapsto a \mapsto b) and p \mapsto a if I remember correctly. (I hope it's not the other way around, i.e. dropping first and adding the top member)

It should be this way. There is no essential need for functional extensionality in the Agda code.

[Ailrun]

Yeah, anyway, let's pass this PR first and then finish those few natrec cases in a separate PR as this one is already quite big.