From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 26 Jan 2014 20:12:59 +0000 (+0000)
Subject: nat: we added a non-indexed theorem
X-Git-Tag: make_still_working~989
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ebf0b4572d0d3252dbbc7b769df676b76bd38c22;hp=ebf0b4572d0d3252dbbc7b769df676b76bd38c22;p=helm.git

nat: we added a non-indexed theorem
lambda: the corrispondence between terms by level and terms by depth
is proved!
---