proposition: Lemma general_omega_shoots_again (A:Type) : forall (v:LList A), general_omega LNil v = general_omega v v.
proof: Proof. simple destruct v. - trivial. - intros; autorewrite with llists using trivial. rewrite general_omega_LNil_LCons; trivial. Qed.
imports: Arith List RelationClasses