proposition: Lemma LAppend_one : forall (A:Type) (a:A) (u v:LList A), LAppend (LCons a u) v = LCons a (LAppend u v).
proof: Proof. cbn in |- *. Abort. Fixpoint LList_decomp_n (A:Type) (n:nat) (l:LList A) {struct n} : LList A := match n with | O => l | S p => match LList_decomp l with | LNil => LNil | LCons a l' => LCons a (LList_decomp_n p l') end end. Lemma LList_decompose_n (A:Type) : forall (n:nat) (l:LList A), l = LList_decomp_n n l. Proof. intros n; induction n as [| n IHn]. - intro l; case l; try reflexivity. - intros l; case l; try trivial. intros a l0; cbn in |- *; rewrite <- IHn; trivial. Qed.
imports: Arith List RelationClasses