proposition: Lemma add1_fix_enumeration: first_derivation (osum2 \1o) =1o (osum2 omega0).
proof: Proof. by move => t ot; rewrite(add_fix_enumeration OS1 ot) (oprod1l OS_omega). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)