till some patches

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

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs.ma
index cf815b7bce6f8677e606784153e1ae32302e3b5a..41de1421556643e20b5f30f0029cb63c446d9da4 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs.ma
@@ -21,6 +21,6 @@ include "T/defs.ma".
 inductive iso: T \to (T \to Prop) \def
 | iso_sort: \forall (n1: nat).(\forall (n2: nat).(iso (TSort n1) (TSort n2)))
 | iso_lref: \forall (i1: nat).(\forall (i2: nat).(iso (TLRef i1) (TLRef i2)))
-| iso_head: \forall (k: K).(\forall (v1: T).(\forall (v2: T).(\forall (t1: 
-T).(\forall (t2: T).(iso (THead k v1 t1) (THead k v2 t2)))))).
+| iso_head: \forall (v1: T).(\forall (v2: T).(\forall (t1: T).(\forall (t2: 
+T).(\forall (k: K).(iso (THead k v1 t1) (THead k v2 t2)))))).