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_vector.ma".
16 include "basic_2/grammar/tsts.ma".
18 (* SAME TOP TERM STRUCTURE **************************************************)
20 (* Advanced inversion lemmas ************************************************)
22 (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
23 lemma tsts_inv_bind_applv_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 →
25 #a #I #Vs #V2 #T1 #T2 #H
26 elim (tsts_inv_pair2 … H) -H #V0 #T0
28 [ #H destruct #H /2 width=5 by simple_inv_bind/
29 | #V #Vs #_ #H destruct