- the confluence of context-senstitive parallel reduction (cpr) is closed!

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / grammar / thom.ma

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 660fff5bf67a479e1de03649ff5d9129ba3cac44..23aa62e03b83a77c5c05629363a538ab685ff995 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma
@@ -16,12 +16,11 @@ include "Basic-2/grammar/term_simple.ma".
 
 (* HOMOMORPHIC TERMS ********************************************************)
 
-inductive thom: term → term → Prop ≝
-   | thom_sort: ∀k. thom (⋆k) (⋆k)
-   | thom_lref: ∀i. thom (#i) (#i)
-   | thom_abst: ∀V1,V2,T1,T2. thom (𝕚{Abst} V1. T1) (𝕚{Abst} V2. T2)
+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] →
-                thom (ð\9d\95\9a{Appl} V1. T1) (ð\9d\95\9a{Appl} V2. T2)
+                thom (ð\9d\95\94{Appl} V1. T1) (ð\9d\95\94{Appl} V2. T2)
 .
 
 interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2).
@@ -49,3 +48,9 @@ lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1].
 /3/ qed.
 
 (* Basic inversion lemmas ***************************************************)
+
+
+(* Basic-1: removed theorems 7:
+            iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans
+            iso_flats_lref_bind_false iso_flats_flat_bind_false
+*)