-ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
- match a with [ mk_pair e1 b1 ⇒
- match b1 with
- [ false ⇒ 〈e1 · \fst b, \snd b〉
- | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]].
+definition item_concat: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
+ λS,i,e.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i \ 5a title="pcat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e, \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e〉.
+
+definition lcat: ∀S:Alpha.∀bcast:(∀S:Alpha.pre S →pre S).pre S → pre S → pre S
+ ≝ λS:Alpha.λbcast:∀S:Alpha.pre S → pre S.λe1,e2:pre S.
+ match e1 with [ mk_pair i1 b1 ⇒ e2].
+
+ match e1 with [ _ => e1].
+
+ match b1 with
+ [ false ⇒ e2 | _ => e1 ]].
+
+ | true ⇒ item_concat S i1 (bcast S e2)
+ ]
+].