(* SIMPLE (NEUTRAL) TERMS ***************************************************)
-inductive simple: term → Prop ≝
+inductive simple: predicate term ≝
| simple_atom: ∀I. simple (𝕒{I})
| simple_flat: ∀I,V,T. simple (𝕗{I} V. T)
.
qed.
lemma simple_inv_bind: ∀I,V,T. 𝕊[𝕓{I} V. T] → False.
-/2 width=6/ qed.
+/2 width=6/ qed-.