coq - シーケンスリストの同等性

Question

lequivColor のライブラリ内 の同等性 ( ) の定義: http://color.inria.fr/doc/CoLoR.Util.List.ListUtil.html

Require Import List.
Variable A : Type.
Definition lequiv (l1 l2: list A) : Prop := l1 [= l2 /\ l2 [= l1.
Infix "[=]" := lequiv (at level 70).

以下の補題を証明したい。これが私の証拠です：

Lemma equiv_app_equiv: forall l1 l2 l3 : list A, l1 ++ l2 [=] l3 -> 
l1 [=] l3 /\ l2 [=] l3.
Proof.
unfold lequiv in |- *; simpl in |- *. intuition.
apply incl_appr_incl in H0. apply H0.

  A : Type
  l1 : list A
  l2 : list A
  l3 : list A
  H0 : l1 ++ l2 [=l3
  H1 : l3 [=l1 ++ l2
  ============================
   l3 [=l1

この目標では、さらに先に進む方法がわかりません。次のようにH1: l3 [= l1 ++ l2書き換えることができる仮説について知りたいl3 [= l1 /\ l3 [= l2です。Coq のライブラリ ( List).

手伝っていただけませんか？私のレンマに何かが欠けていますか？それは証明可能ですか？どうもありがとうございました。

Answer 1