(* *)
(**************************************************************************)
-include "Basic_2/grammar/tshf.ma".
-include "Basic_2/reducibility/tpr.ma".
+include "basic_2/grammar/tshf.ma".
+include "basic_2/reducibility/tpr.ma".
(* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
(* Basic inversion lemmas ***************************************************)
-lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍[T] → T ≈ T.
+lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍⦃T⦄ → T ≈ T.
normalize /2 width=1/
qed-.
]
qed.
-lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T].
-/2 width=1/ qed.
+lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍⦃T⦄.
+/3 width=1/ qed.