(* SIMPLE (NEUTRAL) TERMS ***************************************************)
-inductive simple: term → Prop ≝
- | simple_atom: ∀I. simple (𝕒{I})
- | simple_flat: ∀I,V,T. simple (𝕗{I} V. T)
+inductive simple: predicate term ≝
+ | simple_atom: ∀I. simple (⓪{I})
+ | simple_flat: ∀I,V,T. simple (ⓕ{I} V. T)
.
interpretation "simple (term)" 'Simple T = (simple T).
(* Basic inversion lemmas ***************************************************)
-fact simple_inv_bind_aux: â\88\80T. ð\9d\95\8a[T] â\86\92 â\88\80J,W,U. T = ð\9d\95\93{J} W. U → False.
+fact simple_inv_bind_aux: â\88\80T. ð\9d\90\92[T] â\86\92 â\88\80J,W,U. T = â\93\91{J} W. U → False.
#T * -T
[ #I #J #W #U #H destruct
| #I #V #T #J #W #U #H destruct
]
qed.
-lemma simple_inv_bind: â\88\80I,V,T. ð\9d\95\8a[ð\9d\95\93{I} V. T] → False.
-/2 width=6/ qed.
+lemma simple_inv_bind: â\88\80I,V,T. ð\9d\90\92[â\93\91{I} V. T] → False.
+/2 width=6/ qed-.