Loading theory "HOL-Proofs-Lambda.Commutation" (required by "Locally-Nameless-Sigma.Locally_Nameless_Sigma" via "Locally-Nameless-Sigma.ParRed")
Loading theory "Locally-Nameless-Sigma.Environments" (required by "Locally-Nameless-Sigma.Locally_Nameless_Sigma" via "Locally-Nameless-Sigma.TypedSigma")
### theory "HOL-Proofs-Lambda.Commutation"
### 0.224s elapsed time, 0.536s cpu time, 0.000s GC time
Loading theory "Locally-Nameless-Sigma.ListPre" (required by "Locally-Nameless-Sigma.Locally_Nameless_Sigma" via "Locally-Nameless-Sigma.ParRed" via "Locally-Nameless-Sigma.Sigma" via "Locally-Nameless-Sigma.FMap")
consts
  list_insert ::
    "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list"
### theory "Locally-Nameless-Sigma.ListPre"
### 0.210s elapsed time, 0.420s cpu time, 0.000s GC time
Loading theory "Locally-Nameless-Sigma.FMap" (required by "Locally-Nameless-Sigma.Locally_Nameless_Sigma" via "Locally-Nameless-Sigma.ParRed" via "Locally-Nameless-Sigma.Sigma")
### Ignoring sort constraints in type variables(s): "'a"
### in type abbreviation "fmap"
### Additional type variable(s) in locale specification "inftype": 'a
class inftype = type +
  assumes "infinite": "infinite UNIV"
### theory "Locally-Nameless-Sigma.FMap"
### 0.077s elapsed time, 0.156s cpu time, 0.000s GC time
### Ignoring duplicate elimination (elim)
### \<lbrakk>?P \<le> ?Q; ?P ?x ?y; ?Q ?x ?y \<Longrightarrow> PROP ?W\<rbrakk>
### \<Longrightarrow> PROP ?W
### Ignoring duplicate elimination (elim)
### \<lbrakk>?P \<le> ?Q; ?P ?x ?y; ?Q ?x ?y \<Longrightarrow> PROP ?W\<rbrakk>
### \<Longrightarrow> PROP ?W
consts
  add ::
    "'a environment
     \<Rightarrow> char list \<Rightarrow> 'a \<Rightarrow> 'a environment"
consts
  env_dom :: "'a environment \<Rightarrow> char list set"
consts
  env_get ::
    "'a environment \<Rightarrow> char list \<Rightarrow> 'a option"
consts
  ok :: "'a environment \<Rightarrow> bool"
### Ambiguous input (line 78 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 7 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.env_get"
###       ("\<^const>HOL.Ex_binder" ("_position" T) ("_position" e))
###       ("_position" x))
###     ("_applC" ("_position" Some) ("_position" T))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.Ex_binder" ("_position" T)
###     ("\<^const>HOL.eq" ("\<^const>List.nth" ("_position" e) ("_position" x))
###       ("_applC" ("_position" Some) ("_position" T)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.Ex_binder" ("_position" T)
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.env_get" ("_position" e) ("_position" x))
###       ("_applC" ("_position" Some) ("_position" T)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>HOL.Ex_binder" ("_position" T) ("_position" e))
###     ("\<^const>HOL.eq" ("_position" x)
###       ("_applC" ("_position" Some) ("_position" T)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.Ex_binder" ("_position" T)
###     ("\<^const>Environments.env_get" ("_position" e)
###       ("\<^const>HOL.eq" ("_position" x)
###         ("_applC" ("_position" Some) ("_position" T))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.Ex_binder" ("_position" T)
###     ("_applC"
###       ("\<^const>Environments.env_get" ("_position" e)
###         ("\<^const>HOL.eq" ("_position" x) ("_position" Some)))
###       ("_position" T))))
### ("\<^const>HOL.Trueprop"
###   ("_applC"
###     ("\<^const>Environments.env_get"
###       ("\<^const>HOL.Ex_binder" ("_position" T) ("_position" e))
###       ("\<^const>HOL.eq" ("_position" x) ("_position" Some)))
###     ("_position" T)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 275 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 10 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>HOL.eq" ("\<^const>List.nth" ("_position" e) ("_position" x))
###       ("\<^const>Environments.add" ("_position" e) ("_position" a)
###         ("_position" X)))
###     ("_position" x)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.env_get" ("_position" e) ("_position" x))
###       ("\<^const>Environments.add" ("_position" e) ("_position" a)
###         ("_position" X)))
###     ("_position" x)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>List.nth" ("_position" e)
###     ("\<^const>Environments.env_get"
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X)))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get" ("_position" e)
###     ("\<^const>Environments.env_get"
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X)))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>List.nth"
###     ("\<^const>Environments.env_get" ("_position" e)
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))))
###     ("_position" x)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>Environments.env_get" ("_position" e)
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))))
###     ("_position" x)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("\<^const>List.nth" ("_position" e) ("_position" x))
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add" ("_position" e) ("_position" a)
###         ("_position" X))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.env_get" ("_position" e) ("_position" x))
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add" ("_position" e) ("_position" a)
###         ("_position" X))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get" ("_position" e)
###     ("\<^const>HOL.eq" ("_position" x)
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" x)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.env_get" ("_position" e)
###         ("\<^const>HOL.eq" ("_position" x) ("_position" e)))
###       ("_position" a) ("_position" X))
###     ("_position" x)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 292 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 11 parse trees (10 displayed):
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.env_get" ("_position" e)
###           ("\<^const>HOL.eq" ("_position" x) ("_position" e)))
###         ("_position" a) ("_position" X))
###       ("_position" b) ("_position" Y))
###     ("_position" x)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>HOL.eq" ("\<^const>List.nth" ("_position" e) ("_position" x))
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" b) ("_position" Y)))
###     ("_position" x)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.env_get" ("_position" e) ("_position" x))
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" b) ("_position" Y)))
###     ("_position" x)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>List.nth" ("_position" e)
###     ("\<^const>Environments.env_get"
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" b) ("_position" Y)))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get" ("_position" e)
###     ("\<^const>Environments.env_get"
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" b) ("_position" Y)))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>List.nth"
###     ("\<^const>Environments.env_get" ("_position" e)
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" b) ("_position" Y))))
###     ("_position" x)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>Environments.env_get" ("_position" e)
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" b) ("_position" Y))))
###     ("_position" x)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("\<^const>List.nth" ("_position" e) ("_position" x))
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" b) ("_position" Y))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.env_get" ("_position" e) ("_position" x))
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" b) ("_position" Y))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get" ("_position" e)
###     ("\<^const>HOL.eq" ("_position" x)
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" b) ("_position" Y))
###         ("_position" x)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 296 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 8 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>HOL.eq"
###         ("\<^const>Environments.env_get"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" x))
###         ("_position" e))
###       ("_position" x))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>List.nth"
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("\<^const>HOL.eq" ("_position" x) ("_position" e)))
###       ("_position" x))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("\<^const>HOL.eq" ("_position" x) ("_position" e)))
###       ("_position" x))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add" ("_position" e) ("_position" a)
###         ("_position" X))
###       ("\<^const>Environments.env_get"
###         ("\<^const>HOL.eq" ("_position" x) ("_position" e))
###         ("_position" x)))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" x))
###       ("\<^const>List.nth" ("_position" e) ("_position" x)))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add" ("_position" e) ("_position" a)
###         ("_position" X))
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>List.nth" ("_position" e) ("_position" x))))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" x))
###       ("\<^const>Environments.env_get" ("_position" e) ("_position" x)))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add" ("_position" e) ("_position" a)
###         ("_position" X))
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.env_get" ("_position" e)
###           ("_position" x))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 300 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 8 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" b)
###             ("_applC" ("_position" env_dom) ("_position" e))))
###         ("_asm"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>HOL.not_equal" ("_position" a) ("_position" b)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>HOL.eq"
###         ("\<^const>Environments.env_get"
###           ("\<^const>Environments.add"
###             ("\<^const>Environments.add" ("_position" e) ("_position" a)
###               ("_position" X))
###             ("_position" b) ("_position" Y))
###           ("_position" x))
###         ("_position" e))
###       ("_position" x))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" b)
###             ("_applC" ("_position" env_dom) ("_position" e))))
###         ("_asm"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>HOL.not_equal" ("_position" a) ("_position" b)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>List.nth"
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" b) ("_position" Y))
###         ("\<^const>HOL.eq" ("_position" x) ("_position" e)))
###       ("_position" x))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" b)
###             ("_applC" ("_position" env_dom) ("_position" e))))
###         ("_asm"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>HOL.not_equal" ("_position" a) ("_position" b)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" b) ("_position" Y))
###         ("\<^const>HOL.eq" ("_position" x) ("_position" e)))
###       ("_position" x))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" b)
###             ("_applC" ("_position" env_dom) ("_position" e))))
###         ("_asm"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>HOL.not_equal" ("_position" a) ("_position" b)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" b) ("_position" Y))
###       ("\<^const>Environments.env_get"
###         ("\<^const>HOL.eq" ("_position" x) ("_position" e))
###         ("_position" x)))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" b)
###             ("_applC" ("_position" env_dom) ("_position" e))))
###         ("_asm"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>HOL.not_equal" ("_position" a) ("_position" b)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" b) ("_position" Y))
###         ("_position" x))
###       ("\<^const>List.nth" ("_position" e) ("_position" x)))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" b)
###             ("_applC" ("_position" env_dom) ("_position" e))))
###         ("_asm"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>HOL.not_equal" ("_position" a) ("_position" b)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" b) ("_position" Y))
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>List.nth" ("_position" e) ("_position" x))))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" b)
###             ("_applC" ("_position" env_dom) ("_position" e))))
###         ("_asm"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>HOL.not_equal" ("_position" a) ("_position" b)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" a)
###             ("_position" X))
###           ("_position" b) ("_position" Y))
###         ("_position" x))
###       ("\<^const>Environments.env_get" ("_position" e) ("_position" x)))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.not_member" ("_position" a)
###           ("_applC" ("_position" env_dom) ("_position" e))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" b)
###             ("_applC" ("_position" env_dom) ("_position" e))))
###         ("_asm"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>HOL.not_equal" ("_position" a) ("_position" b)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e) ("_position" a)
###           ("_position" X))
###         ("_position" b) ("_position" Y))
###       ("\<^const>HOL.eq" ("_position" x)
###         ("\<^const>Environments.env_get" ("_position" e)
###           ("_position" x))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 304 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 4 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.not_member" ("_position" xa)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop" ("_applC" ("_position" ok) ("_position" e)))
###       ("_asm"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Environments.env_get"
###             ("\<^const>Environments.add"
###               ("_applC" ("_position" the) ("_position" e)) ("_position" xa)
###               ("_position" U))
###             ("\<^const>HOL.eq" ("_position" xa) ("_position" T)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq" ("_position" U) ("_position" T))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.not_member" ("_position" xa)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop" ("_applC" ("_position" ok) ("_position" e)))
###       ("_asm"
###         ("\<^const>HOL.Trueprop"
###           ("_applC" ("_position" the)
###             ("\<^const>Environments.env_get"
###               ("\<^const>Environments.add" ("_position" e) ("_position" xa)
###                 ("_position" U))
###               ("\<^const>HOL.eq" ("_position" xa) ("_position" T))))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq" ("_position" U) ("_position" T))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.not_member" ("_position" xa)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop" ("_applC" ("_position" ok) ("_position" e)))
###       ("_asm"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>HOL.eq"
###             ("\<^const>Environments.env_get"
###               ("\<^const>Environments.add"
###                 ("_applC" ("_position" the) ("_position" e))
###                 ("_position" xa) ("_position" U))
###               ("_position" xa))
###             ("_position" T))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq" ("_position" U) ("_position" T))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.not_member" ("_position" xa)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop" ("_applC" ("_position" ok) ("_position" e)))
###       ("_asm"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>HOL.eq"
###             ("_applC" ("_position" the)
###               ("\<^const>Environments.env_get"
###                 ("\<^const>Environments.add" ("_position" e)
###                   ("_position" xa) ("_position" U))
###                 ("_position" xa)))
###             ("_position" T))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq" ("_position" U) ("_position" T))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 307 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 4 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.not_member" ("_position" xa)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("_applC" ("_position" ok) ("_position" e)))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" the)
###         ("\<^const>Environments.env_get"
###           ("\<^const>Environments.add" ("_position" e) ("_position" xa)
###             ("_position" U))
###           ("_position" xa)))
###       ("_position" U))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.not_member" ("_position" xa)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("_applC" ("_position" ok) ("_position" e)))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add"
###           ("_applC" ("_position" the) ("_position" e)) ("_position" xa)
###           ("_position" U))
###         ("_position" xa))
###       ("_position" U))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.not_member" ("_position" xa)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("_applC" ("_position" ok) ("_position" e)))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add" ("_position" e) ("_position" xa)
###           ("_position" U))
###         ("\<^const>HOL.eq" ("_position" xa) ("_position" U))))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.not_member" ("_position" xa)
###         ("_applC" ("_position" env_dom) ("_position" e))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("_applC" ("_position" ok) ("_position" e)))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("_applC" ("_position" the) ("_position" e)) ("_position" xa)
###         ("_position" U))
###       ("\<^const>HOL.eq" ("_position" xa) ("_position" U)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 313 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add"
###           ("_applC" ("_position" the) ("_position" e)) ("_position" x)
###           ("_position" A))
###         ("_position" y) ("_position" B))
###       ("_position" x))
###     ("_position" A)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" x)
###             ("_position" A))
###           ("_position" y) ("_position" B))
###         ("_position" x)))
###     ("_position" A)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.add"
###         ("_applC" ("_position" the) ("_position" e)) ("_position" x)
###         ("_position" A))
###       ("_position" y) ("_position" B))
###     ("\<^const>HOL.eq" ("_position" x) ("_position" A))))
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" the)
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e) ("_position" x)
###           ("_position" A))
###         ("_position" y) ("_position" B))
###       ("\<^const>HOL.eq" ("_position" x) ("_position" A)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 322 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add"
###           ("_applC" ("_position" the) ("_position" e)) ("_position" x)
###           ("_position" A))
###         ("_position" y) ("_position" B))
###       ("_position" y))
###     ("_position" B)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.add" ("_position" e) ("_position" x)
###             ("_position" A))
###           ("_position" y) ("_position" B))
###         ("_position" y)))
###     ("_position" B)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_get"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.add"
###         ("_applC" ("_position" the) ("_position" e)) ("_position" x)
###         ("_position" A))
###       ("_position" y) ("_position" B))
###     ("\<^const>HOL.eq" ("_position" y) ("_position" B))))
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" the)
###     ("\<^const>Environments.env_get"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e) ("_position" x)
###           ("_position" A))
###         ("_position" y) ("_position" B))
###       ("\<^const>HOL.eq" ("_position" y) ("_position" B)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Missing patterns in function definition:
### \<And>b. Malformed+b = undefined
### \<And>a. a+Malformed = undefined
Found termination order: "{}"
### Ambiguous input (line 367 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" env_dom)
###       ("\<^const>Groups.plus_class.plus" ("_position" e1) ("_position" e2)))
###     ("\<^const>Set.union" ("_applC" ("_position" env_dom) ("_position" e1))
###       ("_applC" ("_position" env_dom) ("_position" e2)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" env_dom)
###       ("\<^const>Environments.env_app" ("_position" e1) ("_position" e2)))
###     ("\<^const>Set.union" ("_applC" ("_position" env_dom) ("_position" e1))
###       ("_applC" ("_position" env_dom) ("_position" e2)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 380 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 35 parse trees (10 displayed):
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_get"
###         ("\<^const>Groups.plus_class.plus" ("_position" e1)
###           ("_position" e2))
###         ("_position" x)))
###     ("\<^const>List.nth" ("_applC" ("_position" the) ("_position" e1))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_app" ("_position" e1)
###         ("\<^const>Environments.env_get" ("_position" e2) ("_position" x))))
###     ("\<^const>List.nth" ("_applC" ("_position" the) ("_position" e1))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_app" ("_position" e1)
###         ("\<^const>List.nth" ("_position" e2) ("_position" x))))
###     ("\<^const>List.nth" ("_applC" ("_position" the) ("_position" e1))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Groups.plus_class.plus" ("_position" e1)
###         ("\<^const>Environments.env_get" ("_position" e2) ("_position" x))))
###     ("\<^const>List.nth" ("_applC" ("_position" the) ("_position" e1))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Groups.plus_class.plus" ("_position" e1)
###         ("\<^const>List.nth" ("_position" e2) ("_position" x))))
###     ("\<^const>List.nth" ("_applC" ("_position" the) ("_position" e1))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_get"
###         ("\<^const>Environments.env_app" ("_position" e1) ("_position" e2))
###         ("_position" x)))
###     ("\<^const>List.nth" ("_applC" ("_position" the) ("_position" e1))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>List.nth"
###         ("\<^const>Environments.env_app" ("_position" e1) ("_position" e2))
###         ("_position" x)))
###     ("\<^const>List.nth" ("_applC" ("_position" the) ("_position" e1))
###       ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_get"
###         ("\<^const>Groups.plus_class.plus" ("_position" e1)
###           ("_position" e2))
###         ("_position" x)))
###     ("\<^const>Environments.env_get"
###       ("_applC" ("_position" the) ("_position" e1)) ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_app" ("_position" e1)
###         ("\<^const>Environments.env_get" ("_position" e2) ("_position" x))))
###     ("\<^const>Environments.env_get"
###       ("_applC" ("_position" the) ("_position" e1)) ("_position" x))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" the)
###       ("\<^const>Environments.env_app" ("_position" e1)
###         ("\<^const>List.nth" ("_position" e2) ("_position" x))))
###     ("\<^const>Environments.env_get"
###       ("_applC" ("_position" the) ("_position" e1)) ("_position" x))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 396 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" ok)
###     ("\<^const>Groups.plus_class.plus" ("_position" e1) ("_position" e2))))
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" ok)
###     ("\<^const>Environments.env_app" ("_position" e1) ("_position" e2))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 408 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 6 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_app"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.env_app" ("_position" e1) ("_position" e2))
###         ("_position" x) ("_position" X))
###       ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###         ("_position" X)))
###     ("_position" e2)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_app"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.add"
###         ("\<^const>Groups.plus_class.plus" ("_position" e1)
###           ("_position" e2))
###         ("_position" x) ("_position" X))
###       ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###         ("_position" X)))
###     ("_position" e2)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.env_app" ("_position" e1) ("_position" e2))
###       ("_position" x) ("_position" X))
###     ("\<^const>Environments.env_app"
###       ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###         ("_position" X))
###       ("_position" e2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.add"
###       ("\<^const>Groups.plus_class.plus" ("_position" e1) ("_position" e2))
###       ("_position" x) ("_position" X))
###     ("\<^const>Environments.env_app"
###       ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###         ("_position" X))
###       ("_position" e2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.env_app" ("_position" e1) ("_position" e2))
###       ("_position" x) ("_position" X))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###         ("_position" X))
###       ("_position" e2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.add"
###       ("\<^const>Groups.plus_class.plus" ("_position" e1) ("_position" e2))
###       ("_position" x) ("_position" X))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###         ("_position" X))
###       ("_position" e2))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 436 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/Environments.thy") produces 6 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_app"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add"
###           ("\<^const>Groups.plus_class.plus" ("_position" e1)
###             ("_position" e2))
###           ("_position" x) ("_position" X))
###         ("_position" y) ("_position" Y))
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###           ("_position" X))
###         ("_position" y) ("_position" Y)))
###     ("_position" e2)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Environments.env_app"
###     ("\<^const>HOL.eq"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add"
###           ("\<^const>Environments.env_app" ("_position" e1)
###             ("_position" e2))
###           ("_position" x) ("_position" X))
###         ("_position" y) ("_position" Y))
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###           ("_position" X))
###         ("_position" y) ("_position" Y)))
###     ("_position" e2)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.add"
###         ("\<^const>Groups.plus_class.plus" ("_position" e1)
###           ("_position" e2))
###         ("_position" x) ("_position" X))
###       ("_position" y) ("_position" Y))
###     ("\<^const>Environments.env_app"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###           ("_position" X))
###         ("_position" y) ("_position" Y))
###       ("_position" e2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.env_app" ("_position" e1) ("_position" e2))
###         ("_position" x) ("_position" X))
###       ("_position" y) ("_position" Y))
###     ("\<^const>Environments.env_app"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###           ("_position" X))
###         ("_position" y) ("_position" Y))
###       ("_position" e2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.add"
###         ("\<^const>Groups.plus_class.plus" ("_position" e1)
###           ("_position" e2))
###         ("_position" x) ("_position" X))
###       ("_position" y) ("_position" Y))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###           ("_position" X))
###         ("_position" y) ("_position" Y))
###       ("_position" e2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Environments.add"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.env_app" ("_position" e1) ("_position" e2))
###         ("_position" x) ("_position" X))
###       ("_position" y) ("_position" Y))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>Environments.add"
###         ("\<^const>Environments.add" ("_position" e1) ("_position" x)
###           ("_position" X))
###         ("_position" y) ("_position" Y))
###       ("_position" e2))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "Locally-Nameless-Sigma.Environments"
### 1.799s elapsed time, 3.492s cpu time, 0.248s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Locally-Nameless-Sigma/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Locally-Nameless-Sigma/outline -o pdf -n outline -t /proof,/ML
*** Failed to load theory "Locally-Nameless-Sigma.Sigma" (unresolved "Locally-Nameless-Sigma.FMap")
*** Failed to load theory "Locally-Nameless-Sigma.ParRed" (unresolved "Locally-Nameless-Sigma.Sigma")
*** Failed to load theory "Locally-Nameless-Sigma.TypedSigma" (unresolved "Locally-Nameless-Sigma.Sigma")
*** Failed to load theory "Locally-Nameless-Sigma.Locally_Nameless_Sigma" (unresolved "Locally-Nameless-Sigma.ParRed", "Locally-Nameless-Sigma.TypedSigma")
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  (=) F :: ('a \<Rightarrow> 'b option) \<Rightarrow> bool
*** Operand:   {} :: ??'a set
*** 
*** At command "theorem" (line 35 of "~~/afp/thys/Locally-Nameless-Sigma/preliminary/FMap.thy")