Thanks I guess Martin-Löf speaks about W-Types. An implementation and examples in Coq: https://github.com/coq/coq/wiki/WTypeInsteadOfInductiveTypes https://g

Thanks I guess Martin-Löf speaks about W-Types. An implementation and examples in Coq: https://github.com/coq/coq/wiki/WTypeInsteadOfInductiveTypes https://github.com/coq/coq/wiki/WTypeInsteadOfInductiveTypes Still waiting for the year of W-Types