A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.
| Name: | Status: | Subs proved? | Used: |
|---|---|---|---|
| remtau-cont | proved | all subs proved | remtau-pbd, remtau-mon, |
| remtau-mon | proved | all subs proved | |
| remtau-pbd | proved | all subs proved |