(* Advanced properties ******************************************************)
lemma cpmuwe_abbr_neg (h) (n) (G) (L) (T):
- â\88\80V,U. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[h,n] -â\93\93V.U â\86\92 â\9dªG,Lâ\9d« ⊢ T ➡*𝐍𝐖*[h,n] -ⓓV.U.
+ â\88\80V,U. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] -â\93\93V.U â\86\92 â\9d¨G,Lâ\9d© ⊢ T ➡*𝐍𝐖*[h,n] -ⓓV.U.
/3 width=5 by cnuw_abbr_neg, cpmuwe_intro/ qed.
lemma cpmuwe_abst (h) (n) (p) (G) (L) (T):
- â\88\80W,U. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[h,n] â\93\9b[p]W.U â\86\92 â\9dªG,Lâ\9d« ⊢ T ➡*𝐍𝐖*[h,n] ⓛ[p]W.U.
+ â\88\80W,U. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] â\93\9b[p]W.U â\86\92 â\9d¨G,Lâ\9d© ⊢ T ➡*𝐍𝐖*[h,n] ⓛ[p]W.U.
/3 width=5 by cnuw_abst, cpmuwe_intro/ qed.