Meaning of undefx?

[palmskog]

Consider the following alternative definition of undefx in automap.v where the first false is changed to true:

Definition undefx i t := 
  if t is Var n then 
    if onth (varx i) n is Some x then undefb x else true
  else false.

All proofs, at least in fcsl-pcm, pass with this definition. Is there some proof in the full fcsl which proves something about the "vacuous" case when onth (varx i) n = None, or is there some intuition why this case should be false and not true?

[anton-trunov]

AFAIR, we don't care about true/false here because we work under the assumption that interpreted terms are well-formed (there is all (wf i) ts precondition for isundef_sound lemma in the same file), meaning the else case is unreachable.

[palmskog]

OK, I see, thanks!