So through some miracle I was able to prove the theorem (by half baked understanding of simp/autorewrite tactic).

The problem is all the lemmas created by Equations are local and I am not sure how to overwrite that.

I usually have file for code that extracts (I hope that Equations will not end up being extraction disaster) and another file for all theorems/lemmas. and when I import the file that contains the Equations definitions, I cannot access any of the lemmas (hence simp does not work)

Equations names all its lemmas by predictable suffixes to the name you pass to it. If your Equations definition is called `my_def`

, I suggest you do something like `Search "my_def".`

to see lemmas/terms available that were generated by Equations.

Yes they were generated by Equations.

in file called Term.v

I do the following

```
Equations is_weak_value (globs: stringmap Term) (t: Term): bool by wf (size globs) lt := .........
```

simp and funelim works, and I can see all the Equation defined Lemmas in Search.

in model.v I do:

```
From Equations Require Import Equations.
From Packagename Require Import terms.
```

I can see `is_weak_value`

but not the lemmas.

I will try make clean and rebuilt to make sure it is not some cached binaries.

if the file is called `Term.v`

, then the module will be called `Term`

that was a mistake in my typing here!

but apparently make clean & make fixed it somehow.

once again Thanks a lot @Karl Palmskog & @Paolo Giarrusso

walker has marked this topic as resolved.

Last updated: Jan 29 2023 at 05:03 UTC