(* RELOCATION N-STREAM ******************************************************)
-corec definition id: rtmap â\89\9d â\86\91id.
+corec definition id: rtmap â\89\9d ⫯id.
interpretation "identity (nstream)"
'Identity = (id).
(* Basic properties *********************************************************)
-lemma id_rew: â\86\91𝐈𝐝 = 𝐈𝐝.
+lemma id_rew: ⫯𝐈𝐝 = 𝐈𝐝.
<(stream_rew … (𝐈𝐝)) in ⊢ (???%); normalize //
qed.
-lemma id_eq_rew: â\86\91ð\9d\90\88ð\9d\90\9d â\89\97 𝐈𝐝.
+lemma id_eq_rew: ⫯ð\9d\90\88ð\9d\90\9d â\89¡ 𝐈𝐝.
cases id_rew in ⊢ (??%); //
qed.