From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 30 Dec 2012 13:00:21 +0000 (+0000)
Subject: commit completed! some bugs fixed and some instances of auto resized
X-Git-Tag: make_still_working~1370
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=bdff98417627c404aacec8ebb07812287783c500

commit completed! some bugs fixed and some instances of auto resized
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
index e529ee31a..aec82cd5a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
@@ -25,7 +25,7 @@ lemma ltprs_strip: ∀L1. ∀L:term. L ➡* L1 → ∀L2. L ➡ L2 →
 
 (* Main properties **********************************************************)
 
-theorem ltprs_conf: Confluent … ltprs.
+theorem ltprs_conf: confluent … ltprs.
 /3 width=3/ qed.
 
 theorem ltprs_trans: Transitive … ltprs.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma
index 232244510..ec3c9cc57 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma
@@ -27,7 +27,7 @@ lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 →
 (* Main propertis ***********************************************************)
 
 (* Basic_1: was: pr1_confluence *)
-theorem tprs_conf: Confluent … tprs.
+theorem tprs_conf: confluent … tprs.
 /3 width=3/ qed.
 
 (* Basic_1: was: pr1_t *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index 3ff8f21e5..728647926 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -370,7 +370,7 @@ notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ ➡ * break ⦃ term 46 L2
    non associative with precedence 45
    for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }.
 
-notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ Tterm 46 2 ⦄ )"
+notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
    non associative with precedence 45
    for @{ 'PEval $L $T1 $T2 }.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma
index a46c9776b..b5ea1b77e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma
@@ -50,7 +50,7 @@ lemma cfpr_inv_all: ∀L1,L2,L0,T1,T2. L0 ⊢ ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ →
   elim (append_inj_dx … H ?) -H // -HX #_ #H destruct -X
   lapply (ltpss_sn_fwd_length … HL2) >append_length >append_length #H
   lapply (injective_plus_r … H) -H #H
-  @(ex3_1_intro … (⋆.ⓑ{I}V@@Y)) <append_assoc // -HT12
+  @(ex3_intro … (⋆.ⓑ{I}V@@Y)) <append_assoc // -HT12
   <append_assoc [ /3 width=1/ ] -HV1 -HY
   >append_length <associative_plus
   @(ltpss_sn_dx_trans_eq … HL2) -HL2 >H -H >commutative_plus /3 width=1/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
index 22fbfc148..fffaad098 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
@@ -28,7 +28,7 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2.
-/4 width=3/ qed-.
+/3 width=5/ qed-.
 
 (* Basic_1: was by definition: pr2_free *)
 lemma cpr_tpr: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
index 9ff04b705..ae4617f80 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
@@ -157,10 +157,13 @@ lemma cpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
 #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
 elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #T #HTU #T1
 elim (lt_or_ge (|L|) d) #HLd
-[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=2/ ]
+[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK /2 width=2/
+  /3 width=7 by ex2_intro, cpr_intro/
 | elim (lt_or_ge (|L|) (d + e)) #HLde
-  [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=2/ ] 
-  | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK // /5 width=4/
+  [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // /2 width=2/
+    /3 width=7 by ex2_intro, cpr_intro/
+  | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK //
+    /3 width=7 by ex2_intro, cpr_intro/
   ]
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma
index b45dbb99e..a8b117fec 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma
@@ -20,20 +20,23 @@ include "basic_2/reducibility/ltpr_ldrop.ma".
 
 (* Properties about atomic arity assignment on terms ************************)
 
-fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T1 →
-                            ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A.
-#L #T @(fw_ind … L T) -L -T #L #T #IH
-#L1 #T1 #A * -L1 -T1 -A
-[ -IH #L1 #k #H1 #H2 #L2 #_ #T2 #H destruct
-  >(tpr_inv_atom1 … H) -H //
-| #I #L1 #K1 #V1 #B #i #HLK1 #HK1 #H1 #H2 #L2 #HL12 #T2 #H destruct
-  >(tpr_inv_atom1 … H) -T2
+lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ➡ L2 →
+                         ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A.
+#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * *
+[1,2,3:
+  #i #Hn #X #H1 #L2 #HL12 #Y #H2 destruct
+  >(tpr_inv_atom1 … H2) -Y
+|4,5: [ #a ] * #V1 #T1 #Hn #X #H1 #L2 #HL12 #Y #H2 destruct
+]
+[ >(aaa_inv_sort … H1) -X //
+| elim (aaa_inv_lref … H1) #I #K1 #V1 #HLK1 #HA
   lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
-  elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #Y #H #HLK2
   elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
-  lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/
-| #a #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
-  elim (tpr_inv_abbr1 … H) -H *
+  lapply (IH … HKV1 … HA … HK12 … HV12) -L1 -K1 -V1 /2 width=5/
+| elim (aaa_inv_gref … H1)
+| elim (aaa_inv_abbr … H1) -H1 #B #HB #HA
+  elim (tpr_inv_abbr1 … H2) -H2 *
   [ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct
     lapply (tps_lsubs_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2
     lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
@@ -42,30 +45,30 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T
     lapply (IH … HA … (L2.ⓓV1) … HT1) /width=5/ -T1 /2 width=1/ -L1 #HA
     @(aaa_inv_lift … HA … HXT) /2 width=1/
   ]
-| #a #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
-  elim (tpr_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+| elim (aaa_inv_abst … H1) -H1 #B #A #HB #HA #H destruct
+  elim (tpr_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HT12 #H destruct
   lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
   lapply (IH … HA … (L2.ⓛV2) … HT12) -IH -HA -HT12 /width=5/ -T1 /2 width=1/
-| #L1 #V1 #T1 #B #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
-  elim (tpr_inv_appl1 … H) -H *
+| elim (aaa_inv_appl … H1) -H1 #B #HB #HA
+  elim (tpr_inv_appl1 … H2) -H2 *
   [ #V2 #T2 #HV12 #HT12 #H destruct
-    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
-    lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ /2 width=3/
-  | #a #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
-    elim (aaa_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct
-    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
+    lapply (IH … HB … HL12 … HV12) -HB -HV12 /width=5/ #HB
+    lapply (IH … HA … HL12 … HT12) -IH -HA -HL12 -HT12 /width=5/ /2 width=3/
+  | #b #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
+    elim (aaa_inv_abst … HA) -HA #B0 #A0 #HB0 #HA0 #H destruct
+    lapply (IH … HB … HL12 … HV12) -HB -HV12 /width=5/ #HB
     lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
-    lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 [2,4: // |3,5: skip ] /2 width=1/ -T0 -L1 -V1 /4 width=7/
-  | #a #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
-    elim (aaa_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
+    lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 // /2 width=1/ -T0 -L1 -V1 /4 width=7/
+  | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
+    elim (aaa_inv_abbr … HA) -HA #B0 #HW0 #HT0
     lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
-    lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
-    lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 [2,4: // |3,5: skip ] /2 width=1/ -V1 -T0 -L1 -W0 #HT2
+    lapply (IH … HB … HL12 … HV10) -HB -HV10 /width=5/ #HV0
+    lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 // /2 width=1/ -V1 -T0 -L1 -W0 #HT2
     @(aaa_abbr … HW2) -HW2
     @(aaa_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
   ]
-| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
-  elim (tpr_inv_cast1 … H) -H
+| elim (aaa_inv_cast … H1) -H1 #HV1 #HT1
+  elim (tpr_inv_cast1 … H2) -H2
   [ * #V2 #T2 #HV12 #HT12 #H destruct
     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2
     lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/
@@ -75,10 +78,6 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T
 ]
 qed.
 
-lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ➡ L2 →
-                         ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A.
-/2 width=9/ qed.
-
 lemma aaa_ltpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ➡ L2 → L2 ⊢ T ⁝ A.
 /2 width=5/ qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma
index a4bda6daf..cf82cfc37 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma
@@ -196,88 +196,66 @@ qed.
 
 (* Confluence ***************************************************************)
 
-fact tpr_conf_aux:
-   ∀Y0:term. (
-      ∀X0:term. #{X0} < #{Y0} →
-      ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
-      ∃∃X. X1 ➡ X & X2 ➡ X
-         ) →
-   ∀X0,X1,X2. X0 ➡ X1 → X0 ➡ X2 → X0 = Y0 →
-   ∃∃X. X1 ➡ X & X2 ➡ X.
-#Y0 #IH #X0 #X1 #X2 * -X0 -X1
-[ #I1 #H1 #H2 destruct
-  lapply (tpr_inv_atom1 … H1) -H1
+(* Basic_1: was: pr0_confluence *)
+theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 →
+                  ∃∃T. T1 ➡ T & T2 ➡ T.
+#T0 @(f_ind … tw … T0) -T0 #n #IH * 
+[ #I #_ #X1 #X2 #H1 #H2 -n
+  >(tpr_inv_atom1 … H1) -X1
+  >(tpr_inv_atom1 … H2) -X2
 (* case 1: atom, atom *)
-  #H1 destruct //
-| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct
-  elim (tpr_inv_flat1 … H1) -H1 *
-(* case 2: flat, flat *)
-  [ #V2 #T2 #HV02 #HT02 #H destruct
-    /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *)
-(* case 3: flat, beta *)
-  | #b #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct
-    /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *)
-(* case 4: flat, theta *)
-  | #b #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct
-    /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *)
-(* case 5: flat, tau *)
-  | #HT02 #H destruct
-    /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *)
-  ]
-| #a #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct
-  elim (tpr_inv_appl1 … H1) -H1 *
-(* case 6: beta, flat (repeated) *)
-  [ #V2 #T2 #HV02 #HT02 #H destruct
-    @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/
-(* case 7: beta, beta *)
-  | #b #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct
-    /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *)
-(* case 8, beta, theta (excluded) *)
-  | #b #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct
-  ]
-| #a #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct
-  elim (tpr_inv_bind1 … H1) -H1 *
-(* case 9: delta, delta *)
-  [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct
-    /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)
-(* case 10: delta, zeta *)
-  | #T2 #HT20 #HTX2 #H1 #H2 destruct
-    /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
-  ]
-| #a #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct
-  elim (tpr_inv_appl1 … H1) -H1 *
-(* case 11: theta, flat (repeated) *)
-  [ #V2 #T2 #HV02 #HT02 #H destruct
-    @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/
-(* case 12: theta, beta (repeated) *)
-  | #b #V2 #WW0 #TT0 #T2 #_ #_ #H destruct
+  //
+| * [ #a ] #I #V0 #T0 #Hn #X1 #X2 #H1 #H2
+  [ elim (tpr_inv_bind1 … H1) -H1 *
+    [ #V1 #T1 #U1 #HV01 #HT01 #HTU1 #H1
+    | #T1 #HT01 #HXT1 #H11 #H12
+    ]
+    elim (tpr_inv_bind1 … H2) -H2 *
+    [1,3: #V2 #T2 #U2 #HV02 #HT02 #HTU2 #H2
+    |2,4: #T2 #HT02 #HXT2 #H21 #H22
+    ] destruct
+(* case 2: delta, delta *)
+    [ /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)   
+(* case 3: zeta, delta (repeated) *)
+    | @ex2_commute /3 width=10 by tpr_conf_delta_zeta/
+(* case 4: delta, zeta *)
+    | /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
+(* case 5: zeta, zeta *)
+    | /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *)    
+    ]
+  | elim (tpr_inv_flat1 … H1) -H1 *
+    [ #V1 #T1 #HV01 #HT01 #H1
+    | #b1 #V1 #W1 #U1 #T1 #HV01 #HUT1 #H11 #H12 #H13
+    | #b1 #V1 #Y1 #W1 #Z1 #U1 #T1 #HV01 #HWZ1 #HUT1 #HVY1 #H11 #H12 #H13
+    | #HX1 #H1
+    ]
+    elim (tpr_inv_flat1 … H2) -H2 *
+    [1,5,9,13: #V2 #T2 #HV02 #HT02 #H2
+    |2,6,10,14: #b2 #V2 #W2 #U2 #T2 #HV02 #HUT2 #H21 #H22 #H23
+    |3,7,11,15: #b2 #V2 #Y2 #W2 #Z2 #U2 #T2 #HV02 #HWZ2 #HUT2 #HVY2 #H21 #H22 #H23
+    |4,8,12,16: #HX2 #H2
+    ] destruct
+(* case 6: flat, flat *)
+    [ /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *)
+(* case 7: beta, flat (repeated) *)
+    | @ex2_commute /3 width=8 by tpr_conf_flat_beta/
+(* case 8: theta, flat (repeated) *)
+    | @ex2_commute /3 width=11 by tpr_conf_flat_theta/
+(* case 9: tau, flat (repeated) *)
+    | @ex2_commute /3 width=6 by tpr_conf_flat_cast/
+(* case 10: flat, beta *)
+    | /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *)
+(* case 11: beta, beta *)
+    | /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *)
+(* case 12: flat, theta *)
+    | /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *)
 (* case 13: theta, theta *)
-  | #b #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct
-    /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *)
-  ]
-| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct
-  elim (tpr_inv_abbr1 … H1) -H1 *
-(* case 14: zeta, delta (repeated) *)
-  [ #V2 #TT2 #T2 #HV02 #HTT02 #HTT2 #H destruct
-    @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/
-(* case 15: zeta, zeta *)
-  | #TT2 #HTT02 #HXTT2
-    /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *)
-  ]
-| #V0 #T0 #T1 #HT01 #H1 #H2 destruct
-  elim (tpr_inv_cast1 … H1) -H1
-(* case 16: tau, flat (repeated) *)
-  [ * #V2 #T2 #HV02 #HT02 #H destruct
-    @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/
-(* case 17: tau, tau *)
-  | #HT02
-    /3 width=5 by tpr_conf_tau_tau/
+    | /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *)
+(* case 14: flat, tau *)
+    | /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *)
+(* case 15: tau, tau *)
+    | /3 width=5 by tpr_conf_tau_tau/
+    ]
   ]
 ]
 qed.
-
-(* Basic_1: was: pr0_confluence *)
-theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 →
-                  ∃∃T. T1 ➡ T & T2 ➡ T.
-#T @(tw_ind … T) -T /3 width=6 by tpr_conf_aux/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
index 7b4813491..b5f416344 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
@@ -63,6 +63,20 @@ lemma aaa_inv_lref: ∀L,A,i. L ⊢ #i ⁝ A →
                     ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A.
 /2 width=3/ qed-.
 
+fact aaa_inv_gref_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀p. T = §p → ⊥.
+#L #T #A * -L -T -A
+[ #L #k #q #H destruct
+| #I #L #K #V #B #i #HLK #HB #q #H destruct
+| #a #L #V #T #B #A #_ #_ #q #H destruct
+| #a #L #V #T #B #A #_ #_ #q #H destruct
+| #L #V #T #B #A #_ #_ #q #H destruct
+| #L #V #T #A #_ #_ #q #H destruct
+]
+qed.
+
+lemma aaa_inv_gref: ∀L,A,p. L ⊢ §p ⁝ A → ⊥.
+/2 width=6/ qed-.
+
 fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀a,W,U. T = ⓓ{a}W. U →
                        ∃∃B. L ⊢ W ⁝ B & L. ⓓW ⊢ U ⁝ A.
 #L #T #A * -L -T -A