X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftwhnf.ma;h=6284eaa0b9a9c8b0f1cde079ccf5704f34b4aa05;hb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;hp=90598b1e7905bcf8639d2fdffc83841f1dcf4272;hpb=eb918fc784eacd2094e3986ba321ef47690d9983;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma
index 90598b1e7..6284eaa0b 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/tshf.ma".
-include "Basic_2/reducibility/tpr.ma".
+include "basic_2/grammar/tshf.ma".
+include "basic_2/reducibility/tpr.ma".
 
 (* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
 
@@ -25,7 +25,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍[T] → T ≈ T.
+lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍⦃T⦄ → T ≈ T.
 normalize /2 width=1/
 qed-.
 
@@ -37,20 +37,20 @@ lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2.
   elim (tshf_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct
   lapply (IHT12 HT1U2) -IHT12 -HT1U2 #HUT2
   lapply (simple_tshf_repl_dx … HUT2 HT1) /2 width=1/
-| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+| #a #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
   elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #H
   elim (simple_inv_bind … H)
-| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H
-  elim (tshf_inv_bind1 … H) -H #W2 #U2 #H destruct //
-| #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H
+  elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct //
+| #a #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
   elim (tshf_inv_flat1 … H) -H #U1 #U2 #_ #H
   elim (simple_inv_bind … H)
 | #V #T #T1 #T2 #_ #_ #_ #H
-  elim (tshf_inv_bind1 … H) -H #W2 #U2 #H destruct
+  elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct
 | #V #T1 #T2 #_ #_ #H
   elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct
 ]
 qed.
 
-lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T].
-/2 width=1/ qed.
+lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍⦃T⦄.
+/3 width=1/ qed.