- we polarized binders to control zeta reduction

[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..6284eaa0b9a9c8b0f1cde079ccf5704f34b4aa05 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma
@@ -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.