(* 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] →