proposition: Theorem Forall2_app_inv_r : forall l1' l2' l, Forall2 l (l1' ++ l2') -> exists l1 l2, Forall2 l1 l1' /\ Forall2 l2 l2' /\ l = l1 ++ l2.
proof: Proof. intro l1'; induction l1' as [|a l1' IHl1']; intros l2' l H. - exists [], l; auto. - simpl in H; inversion H as [|x ? ? ? ? H4]; subst; clear H. apply IHl1' in H4 as (l1 & l2 & Hl1 & Hl2 & ->). exists (x::l1), l2; simpl; auto. Qed.
imports: PeanoNat