(* HOMOMORPHIC TERMS ********************************************************)
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: â\88\80V1,V2,T1,T2. thom T1 T2 â\86\92 ð\9d\95\8a[T1] â\86\92 ð\9d\95\8a[T2] →
- thom (𝕔{Appl} V1. T1) (𝕔{Appl} V2. T2)
+ | thom_atom: ∀I. thom (⓪{I}) (⓪{I})
+ | thom_abst: ∀V1,V2,T1,T2. thom (ⓛV1. T1) (ⓛV2. T2)
+ | thom_appl: â\88\80V1,V2,T1,T2. thom T1 T2 â\86\92 ð\9d\90\92[T1] â\86\92 ð\9d\90\92[T2] →
+ thom (ⓐV1. T1) (ⓐV2. T2)
.
interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2).
lemma thom_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1.
/3 width=2/ qed.
-lemma simple_thom_repl_dx: â\88\80T1,T2. T1 â\89\88 T2 â\86\92 ð\9d\95\8a[T1] â\86\92 ð\9d\95\8a[T2].
+lemma simple_thom_repl_dx: â\88\80T1,T2. T1 â\89\88 T2 â\86\92 ð\9d\90\92[T1] â\86\92 ð\9d\90\92[T2].
#T1 #T2 #H elim H -T1 -T2 //
#V1 #V2 #T1 #T2 #H
elim (simple_inv_bind … H)
qed. (**) (* remove from index *)
-lemma simple_thom_repl_sn: â\88\80T1,T2. T1 â\89\88 T2 â\86\92 ð\9d\95\8a[T2] â\86\92 ð\9d\95\8a[T1].
+lemma simple_thom_repl_sn: â\88\80T1,T2. T1 â\89\88 T2 â\86\92 ð\9d\90\92[T2] â\86\92 ð\9d\90\92[T1].
/3 width=3/ qed-.
(* Basic inversion lemmas ***************************************************)
-fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕓{I}W1.U1 →
- ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2.
+fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓑ{I}W1.U1 →
+ ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
#T1 #T2 * -T1 -T2
[ #J #I #W1 #U1 #H destruct
| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
]
qed.
-lemma thom_inv_bind1: ∀I,W1,U1,T2. 𝕓{I}W1.U1 ≈ T2 →
- ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2.
+lemma thom_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 →
+ ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
/2 width=5/ qed-.
-fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕗{I}W1.U1 →
- â\88\83â\88\83W2,U2. U1 â\89\88 U2 & ð\9d\95\8a[U1] & ð\9d\95\8a[U2] &
- I = Appl & T2 = 𝕔{Appl} W2. U2.
+fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
+ â\88\83â\88\83W2,U2. U1 â\89\88 U2 & ð\9d\90\92[U1] & ð\9d\90\92[U2] &
+ I = Appl & T2 = ⓐW2. U2.
#T1 #T2 * -T1 -T2
[ #J #I #W1 #U1 #H destruct
| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
]
qed.
-lemma thom_inv_flat1: ∀I,W1,U1,T2. 𝕗{I}W1.U1 ≈ T2 →
- â\88\83â\88\83W2,U2. U1 â\89\88 U2 & ð\9d\95\8a[U1] & ð\9d\95\8a[U2] &
- I = Appl & T2 = 𝕔{Appl} W2. U2.
+lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
+ â\88\83â\88\83W2,U2. U1 â\89\88 U2 & ð\9d\90\92[U1] & ð\9d\90\92[U2] &
+ I = Appl & T2 = ⓐW2. U2.
/2 width=4/ qed-.
(* Basic_1: removed theorems 7: