rec definition fold L T on L ≝ match L with
[ LAtom ⇒ T
| LBind L I ⇒ match I with
- [ BUnit _ ⇒ fold L (-ⓛ⋆0.T)
+ [ BUnit _ ⇒ fold L (-ⓛ⋆𝟎.T)
| BPair I V ⇒ fold L (-ⓑ[I]V.T)
]
].
lemma fold_atom: ∀T. ⋆ + T = T.
// qed.
-lemma fold_unit: ∀I,L,T. L.ⓤ[I]+T = L+(-ⓛ⋆0.T).
+lemma fold_unit: ∀I,L,T. L.ⓤ[I]+T = L+(-ⓛ⋆𝟎.T).
// qed.
lemma fold_pair: ∀I,L,V,T. (L.ⓑ[I]V)+T = L+(-ⓑ[I]V.T).