firs error: iso/props

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / T / defs.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma
index 42d3dcb191a94b838db0d6cf5a2269bd87e29491..cf483de06c4a16a6dd2868497a150cd74195d7a8 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma
@@ -47,3 +47,7 @@ definition THeads:
 T).(match us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u 
 (THeads k ul t))])) in THeads.
 
+inductive C: Set \def
+| CSort: nat \to C
+| CHead: C \to (K \to (T \to C)).
+