X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftwhnf.ma;h=5125fbb0e6317c74ac0b2edd64e841581fe9aa09;hb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;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..5125fbb0e 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-.
 
@@ -52,5 +52,5 @@ lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2.
 ]
 qed.
 
-lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T].
-/2 width=1/ qed.
+lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍⦃T⦄.
+/3 width=1/ qed.