proposition: Lemma general_omega_LNil_LCons (A:Type): forall (a:A) (u:LList A), general_omega LNil (LCons a u) = LCons a (general_omega u (LCons a u)).
proof: Proof. intros a u; LList_unfold (general_omega LNil (LCons a u)); trivial. Qed.
imports: Arith List RelationClasses