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 "static_2/syntax/theq.ma".
16 include "static_2/relocation/lifts_lifts.ma".
18 (* GENERIC RELOCATION FOR TERMS *********************************************)
20 (* Properties with tail sort-irrelevant head equivalence for terms **********)
22 lemma theq_lifts_bi: liftable2_bi theq.
23 #T1 #T2 #H elim H -T1 -T2 [||| * ]
24 [ #s1 #s2 #f #X1 #H1 #X2 #H2
25 >(lifts_inv_sort1 … H1) -H1 >(lifts_inv_sort1 … H2) -H2
26 /1 width=1 by theq_sort/
27 | #i #f #X1 #H1 #X2 #H2
28 elim (lifts_inv_lref1 … H1) -H1 #j1 #Hj1 #H destruct
29 elim (lifts_inv_lref1 … H2) -H2 #j2 #Hj2 #H destruct
30 <(at_mono … Hj2 … Hj1) -i -f -j2
31 /1 width=1 by theq_lref/
32 | #l #f #X1 #H1 #X2 #H2
33 >(lifts_inv_gref1 … H1) -H1 >(lifts_inv_gref1 … H2) -H2
34 /1 width=1 by theq_gref/
35 | #p #I #V1 #V2 #T1 #T2 #f #X1 #H1 #X2 #H2
36 elim (lifts_inv_bind1 … H1) -H1 #W1 #U1 #_ #_ #H destruct
37 elim (lifts_inv_bind1 … H2) -H2 #W2 #U2 #_ #_ #H destruct
38 /1 width=1 by theq_pair/
39 | #I #V1 #V2 #T1 #T2 #f #X1 #H1 #X2 #H2
40 elim (lifts_inv_flat1 … H1) -H1 #W1 #U1 #_ #_ #H destruct
41 elim (lifts_inv_flat1 … H2) -H2 #W2 #U2 #_ #_ #H destruct
42 /1 width=1 by theq_pair/
46 (* Inversion lemmas with tail sort-irrelevant head equivalence for terms ****)
48 lemma theq_inv_lifts_bi: deliftable2_bi theq.
49 #U1 #U2 #H elim H -U1 -U2 [||| * ]
50 [ #s1 #s2 #f #X1 #H1 #X2 #H2
51 >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2
52 /1 width=1 by theq_sort/
53 | #j #f #X1 #H1 #X2 #H2
54 elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
55 elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
56 <(at_inj … Hj2 … Hj1) -j -f -i1
57 /1 width=1 by theq_lref/
58 | #l #f #X1 #H1 #X2 #H2
59 >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
60 /1 width=1 by theq_gref/
61 | #p #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
62 elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct
63 elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct
64 /1 width=1 by theq_pair/
65 | #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
66 elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #_ #H destruct
67 elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #_ #H destruct
68 /1 width=1 by theq_pair/