X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fthnf.ma;h=ab864268f22aa37c5f91b043236560d0defe7e5c;hb=bde429ac54e48de74b3d8b1df72dfcb86aa9bae5;hp=b271a112b43f6a48e05f32c36e8e5645ee70ca7c;hpb=439b6ec33d749ba4e6ae0938e973a85bc23e306e;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma
index b271a112b..ab864268f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma
@@ -25,7 +25,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma twhnf_inv_tshf: ∀T. 𝐇𝐍⦃T⦄ → T ≈ T.
+lemma thnf_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⦄.
+lemma thnf_tshf: ∀T. T ≈ T → 𝐇𝐍⦃T⦄.
 /3 width=1/ qed.