rec definition flifts f U on U ≝ match U with
[ TAtom I ⇒ match I with
[ Sort _ ⇒ U
- | LRef i â\87\92 #(f@â\9d´iâ\9dµ)
+ | LRef i â\87\92 #(f@â\9d¨iâ\9d©)
| GRef _ ⇒ U
]
| TPair I V T ⇒ match I with
- [ Bind2 p I ⇒ ⓑ{p,I}(flifts f V).(flifts (⫯f) T)
- | Flat2 I ⇒ ⓕ{I}(flifts f V).(flifts f T)
+ [ Bind2 p I ⇒ ⓑ[p,I](flifts f V).(flifts (⫯f) T)
+ | Flat2 I ⇒ ⓕ[I](flifts f V).(flifts f T)
]
].
(* Basic properties *********************************************************)
-lemma flifts_lref (f) (i): â\86\91*[f](#i) = #(f@â\9d´iâ\9dµ).
+lemma flifts_lref (f) (i): â\86\91*[f](#i) = #(f@â\9d¨iâ\9d©).
// qed.
-lemma flifts_bind (f) (p) (I) (V) (T): ↑*[f](ⓑ{p,I}V.T) = ⓑ{p,I}↑*[f]V.↑*[⫯f]T.
+lemma flifts_bind (f) (p) (I) (V) (T): ↑*[f](ⓑ[p,I]V.T) = ⓑ[p,I]↑*[f]V.↑*[⫯f]T.
// qed.
-lemma flifts_flat (f) (I) (V) (T): ↑*[f](ⓕ{I}V.T) = ⓕ{I}↑*[f]V.↑*[f]T.
+lemma flifts_flat (f) (I) (V) (T): ↑*[f](ⓕ[I]V.T) = ⓕ[I]↑*[f]V.↑*[f]T.
// qed.
(* Main properties **********************************************************)