Anton Salikhmetov

Yes, that is still the case: ``` (f: f (f (x: x))) (i: (f: f (x: x) (f (x: x))) (x: (h, u: h (h u)) (y: x (i y))))...

I just realized that the following information might be useful in investigation. By adding some debug output: ``` diff --git a/encoding/abstract/template.txt b/encoding/abstract/template.txt index 27b2b6b..a6ac35b 100644 --- a/encoding/abstract/template.txt +++ b/encoding/abstract/template.txt @@...

It is true that the embedded read-back mechanism can only retrieve the β-normal form of a term (if any). As for keeping track of the evaluated term during reduction, it...