Re: [FLD] review of Appendix Hebrand Structures

<snip/>

> 2- In the definition of Herbrand domain, it seems to me that the second
> and
> > third bullet are redundant, since they are implied by the first
>
> Why? These terms (mentioned in those bullets) are equal according to our
> semantics. How does it follow that they are equal in Herbrand structures if
> those bullets are not included?
>

They are indeed equal to our semantics, so if t and s are such equal terms,
then TVal_I(s=t) must be true, so (s,t)\in E, by the first bullet.


<snip/>