]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/G/defs.ma
new theorems
[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / G / defs.ma
index c493641aaceaf41b663a21ecebc35b7a9d3c1cf2..bc601b30942b4b1343b6010186b80d0da2ecd47a 100644 (file)
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/G/defs".
 
-include "../Base/theory.ma".
+include "preamble.ma".
 
 record G : Set \def {
  next: (nat \to nat);