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