(* Basic inversion lemmas ***************************************************)
-lemma twhnf_inv_tshf: ∀T. 𝐇𝐍⦃T⦄ → T ≈ T.
+lemma thnf_inv_tshf: ∀T. 𝐇𝐍⦃T⦄ → T ≈ T.
normalize /2 width=1/
qed-.
]
qed.
-lemma twhnf_tshf: ∀T. T ≈ T → 𝐇𝐍⦃T⦄.
+lemma thnf_tshf: ∀T. T ≈ T → 𝐇𝐍⦃T⦄.
/3 width=1/ qed.