proposition: Lemma Rmessages_app_bwd : forall ms2 ms ms1, Rmessages ms (ms1 ++ ms2) -> exists ms11 ms12, ms = ms11 ++ ms12 /\ Rmessages ms11 ms1 /\ Rmessages ms12 ms2.
proof: Proof. induction ms; destruct ms1; simpl; inversion 1; subst. exists nil; exists nil; eauto. exists nil; exists (a :: ms); eauto. apply IHms in H8; firstorder subst. exists (a :: x); exists x0; eauto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)