- a caracterization of the top elements of the local evironment

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / twhnf.ma

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 687893b9082b5f4549212c5657216ecdae6e108d..2a5e62f3444e8a013381e2c91b8c5459d20eb72f 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma
@@ -53,4 +53,4 @@ lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2.
 qed.
 
 lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T].
-/2 width=1/ qed.
+/3 width=1/ qed.