]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambda/policy.txt
- lambda: - normalization theorem completed!
[helm.git] / matita / matita / contribs / lambda / policy.txt
index ef8c96fce518c20b368e1aa0e66604e09d0b2a6c..987d9f8b194b20631ea81e8f5d79d6ed18827407 100644 (file)
@@ -4,6 +4,7 @@ A, B, C, D: term
 H         : transient premise
 IH        : inductive premise
 M, N      : term
+P, Q      : pointer tree
 R         : arbitrary relation
 T, U      : arbitrary small type