inductive thom: relation term ≝
| thom_atom: ∀I. thom (⓪{I}) (⓪{I})
| thom_abst: ∀V1,V2,T1,T2. thom (ⓛV1. T1) (ⓛV2. T2)
inductive thom: relation term ≝
| 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\95\8a[T1] â\86\92 ð\9d\95\8a[T2] →
+ | thom_appl: â\88\80V1,V2,T1,T2. thom T1 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 *)
#T1 #T2 #H elim H -T1 -T2 //
#V1 #V2 #T1 #T2 #H
elim (simple_inv_bind … H)
qed. (**) (* remove from index *)
/2 width=5/ qed-.
fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
/2 width=5/ qed-.
fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
qed.
lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
qed.
lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →