proposition: Lemma L6 : forall n, LNth n (LAppend u v) = Some 1.
proof: Proof. intro n; transitivity (LNth n u). - apply bisimilar_LNth. generalize (bisimilar_sym (A:=nat));intro H;apply H. apply L4. - apply L5. Qed.
imports: chap13