X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_teqx.ma;h=130d42c6a3c9b4192f089fdf0f4aee331e2191c5;hp=789e4c4ebda50cbb2f90a50a4b07fe724877e12d;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hpb=613d8642b1154dde0c026cbdcd96568910198251

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqx.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqx.ma
index 789e4c4eb..130d42c6a 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqx.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqx.ma
@@ -12,79 +12,33 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "static_2/relocation/lifts_teqg.ma".
 include "static_2/syntax/teqx.ma".
-include "static_2/relocation/lifts_lifts.ma".
 
 (* GENERIC RELOCATION FOR TERMS *********************************************)
 
 (* Properties with sort-irrelevant equivalence for terms ********************)
 
 lemma teqx_lifts_sn: liftable2_sn teqx.
-#T1 #T2 #H elim H -T1 -T2 [||| * ]
-[ #s1 #s2 #f #X #H >(lifts_inv_sort1 … H) -H
-  /3 width=3 by lifts_sort, teqx_sort, ex2_intro/
-| #i #f #X #H elim (lifts_inv_lref1 … H) -H
-  /3 width=3 by lifts_lref, teqx_lref, ex2_intro/
-| #l #f #X #H >(lifts_inv_gref1 … H) -H
-  /2 width=3 by lifts_gref, teqx_gref, ex2_intro/
-| #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H elim (lifts_inv_bind1 … H) -H
-  #W1 #U1 #HVW1 #HTU1 #H destruct
-  elim (IHV … HVW1) -V1 elim (IHT … HTU1) -T1
-  /3 width=5 by lifts_bind, teqx_pair, ex2_intro/
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H elim (lifts_inv_flat1 … H) -H
-  #W1 #U1 #HVW1 #HTU1 #H destruct
-  elim (IHV … HVW1) -V1 elim (IHT … HTU1) -T1
-  /3 width=5 by lifts_flat, teqx_pair, ex2_intro/
-]
-qed-.
+/2 width=3 by teqg_lifts_sn/ qed-.
 
 lemma teqx_lifts_dx: liftable2_dx teqx.
-/3 width=3 by teqx_lifts_sn, liftable2_sn_dx, teqx_sym/ qed-.
+/2 width=3 by teqg_lifts_dx/ qed-.
 
 lemma teqx_lifts_bi: liftable2_bi teqx.
-/3 width=6 by teqx_lifts_sn, liftable2_sn_bi/ qed-.
+/2 width=6 by teqg_lifts_bi/ qed-.
 
 (* Inversion lemmas with sort-irrelevant equivalence for terms **************)
 
 lemma teqx_inv_lifts_sn: deliftable2_sn teqx.
-#U1 #U2 #H elim H -U1 -U2 [||| * ]
-[ #s1 #s2 #f #X #H >(lifts_inv_sort2 … H) -H
-  /3 width=3 by lifts_sort, teqx_sort, ex2_intro/
-| #i #f #X #H elim (lifts_inv_lref2 … H) -H
-  /3 width=3 by lifts_lref, teqx_lref, ex2_intro/
-| #l #f #X #H >(lifts_inv_gref2 … H) -H
-  /2 width=3 by lifts_gref, teqx_gref, ex2_intro/
-| #p #I #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X #H elim (lifts_inv_bind2 … H) -H
-  #V1 #T1 #HVW1 #HTU1 #H destruct
-  elim (IHW … HVW1) -W1 elim (IHU … HTU1) -U1
-  /3 width=5 by lifts_bind, teqx_pair, ex2_intro/
-| #I #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X #H elim (lifts_inv_flat2 … H) -H
-  #V1 #T1 #HVW1 #HTU1 #H destruct
-  elim (IHW … HVW1) -W1 elim (IHU … HTU1) -U1
-  /3 width=5 by lifts_flat, teqx_pair, ex2_intro/
-]
-qed-.
+/2 width=3 by teqg_inv_lifts_sn/ qed-.
 
 lemma teqx_inv_lifts_dx: deliftable2_dx teqx.
-/3 width=3 by teqx_inv_lifts_sn, deliftable2_sn_dx, teqx_sym/ qed-.
+/2 width=3 by teqg_inv_lifts_dx/ qed-.
 
 lemma teqx_inv_lifts_bi: deliftable2_bi teqx.
-/3 width=6 by teqx_inv_lifts_sn, deliftable2_sn_bi/ qed-.
+/2 width=6 by teqg_inv_lifts_bi/ qed-.
 
 lemma teqx_lifts_inv_pair_sn (I) (f):
-      ∀X,T. ⇧*[f]X ≘ T → ∀V. ②[I]V.T ≛ X → ⊥.
-#I #f #X #T #H elim H -f -X -T
-[ #f #s #V #H
-  elim (teqx_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct
-| #f #i #j #_ #V #H
-  elim (teqx_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct
-| #f #l #V #H
-  elim (teqx_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct
-| #f #p #J #X1 #T1 #X2 #T2 #_ #_ #_ #IH2 #V #H
-  elim (teqx_inv_pair1 … H) -H #Z1 #Z2 #_ #HZ2 #H destruct
-  /2 width=2 by/
-| #f #J #X1 #T1 #X2 #T2 #_ #_ #_ #IH2 #V #H
-  elim (teqx_inv_pair1 … H) -H #Z1 #Z2 #_ #HZ2 #H destruct
-  /2 width=2 by/
-]
-qed-.
+      ∀X,T. ⇧*[f]X ≘ T → ∀V. ②[I]V.T ≅ X → ⊥.
+/2 width=8 by teqg_lifts_inv_pair_sn/ qed-.