X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_structure_depth.ma;h=4648217932fcd1d310c88dc807afa8f64f622b45;hb=3c78efa39d4783f83638b1aabe8d776d83aabf35;hp=700da6a46e26d3c6e5f8c6b4b3ac0be0425a571c;hpb=d08b01eee540a6e955cb12cb7421da4198a4ef48;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma index 700da6a46..464821793 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma @@ -20,7 +20,7 @@ include "delayed_updating/syntax/path_depth.ma". (* Constructions with depth *************************************************) lemma depth_structure (p): - ❘p❘ = ❘⊗p❘. + ♭p = ♭⊗p. #p elim p -p // * [ #n ] #p #IH // [