[FRIAM] theoremdep

[glen]

I've slept since we had the thread about lemma concatenation. But this seems relevant:

https://philpapers.org/rec/BARAHO-17?ref=mail
"In other words, if cumulative deductive progress is not guaranteed, we cannot be sure that lemmas are knowledge checkpoints. But this seems quite an important property of classical reasoning, while it certainly is not a feature of reasoning carried out in ST."
-- 
glen