1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/grammar/term.ma".
17 (* SIMPLE (NEUTRAL) TERMS ***************************************************)
19 inductive simple: predicate term ≝
20 | simple_atom: ∀I. simple (⓪{I})
21 | simple_flat: ∀I,V,T. simple (ⓕ{I} V. T)
24 interpretation "simple (term)" 'Simple T = (simple T).
26 (* Basic inversion lemmas ***************************************************)
28 lemma mt: ∀R1,R2:Prop. (R1 → R2) → (R2 → ⊥) → R1 → ⊥.
31 fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀a,J,W,U. T = ⓑ{a,J} W. U → ⊥.
33 [ #I #a #J #W #U #H destruct
34 | #I #V #T #a #J #W #U #H destruct
38 lemma simple_inv_bind: ∀a,I,V,T. 𝐒⦃ⓑ{a,I} V. T⦄ → ⊥.
39 /2 width=7/ qed-. (**) (* auto fails if mt is enabled *)
41 lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J.
42 * /2 width=2/ #a #I #V #T #H
43 elim (simple_inv_bind … H)