]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/defs.ma
new makefiles
[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / getl / defs.ma
index 40845209b3b003b54ad9aa803d693c109b0818ac..8c40f88323598c1498d13e8b1cd75c95b208f031 100644 (file)
@@ -20,7 +20,7 @@ include "drop/defs.ma".
 
 include "clear/defs.ma".
 
-inductive getl (h:nat) (c1:C) (c2:C): Prop \def
+inductive getl (h: nat) (c1: C) (c2: C): Prop \def
 | getl_intro: \forall (e: C).((drop h O c1 e) \to ((clear e c2) \to (getl h 
 c1 c2))).