(* Basic inversion lemmas ***************************************************)
-lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍[T] → T ≈ T.
+lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍⦃T⦄ → T ≈ T.
normalize /2 width=1/
qed-.
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].
+lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍⦃T⦄.
/3 width=1/ qed.