X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fgrammar%2Fthom.ma;h=23aa62e03b83a77c5c05629363a538ab685ff995;hb=95fe49b9bd546ee4f0d27dce7267d7285eb81b01;hp=876bd7fd9f7ee9a685e8a401437a0c09e8eb3d33;hpb=cd0870e2572a77bd69bda4b8c403c30b569c58b9;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma
index 876bd7fd9..23aa62e03 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma
@@ -16,7 +16,7 @@ include "Basic-2/grammar/term_simple.ma".
 
 (* HOMOMORPHIC TERMS ********************************************************)
 
-inductive thom: term → term → Prop ≝
+inductive thom: relation term ≝
    | thom_atom: ∀I. thom (𝕒{I}) (𝕒{I})
    | thom_abst: ∀V1,V2,T1,T2. thom (𝕔{Abst} V1. T1) (𝕔{Abst} V2. T2)
    | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝕊[T1] → 𝕊[T2] →