proposition: Lemma general_omega_LCons (A:Type) : forall (a:A) (u v:LList A), general_omega (LCons a u) v = LCons a (general_omega u v).
proof: Proof. intros a u v; LList_unfold (general_omega (LCons a u) v); case v; cbn in |- *; auto. now rewrite general_omega_LNil. Qed.
imports: Arith List RelationClasses