(* Basic_1: was just: sn3_nf2 *)
lemma cnx_csx (G) (L):
- â\88\80T. â\9dªG,Lâ\9d« â\8a¢ â¬\88ð\9d\90\8d T â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 T.
+ â\88\80T. â\9d¨G,Lâ\9d© â\8a¢ â¬\88ð\9d\90\8d T â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 T.
/2 width=1 by NF_to_SN/ qed.
(* Advanced properties ******************************************************)
lemma csx_sort (G) (L):
- â\88\80s. â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 ⋆s.
+ â\88\80s. â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 ⋆s.
/3 width=4 by cnx_csx, cnx_sort/ qed.