proposition: Lemma from_q0 : forall t:LList acts, Trace A1 q0 t -> exists t' : LList acts, Trace A1 q2 t' /\ (t = LCons a (LCons a t') \/ t = LCons b (LCons a t')).
proof: Proof. intros t H; inversion_clear H. - case (no_deadlocks H0). - generalize H0 H1; case a0; cbn in |- *. + do 2 simple destruct 1. intro H3; case (from_q1 H3). intros x [H4 H5]; exists x; auto. rewrite H5; auto. + do 2 simple destruct 1. intro H3; case (from_q1 H3); intros x [H4 H5]. exists x; auto. rewrite H5; auto. Qed.
imports: Arith List RelationClasses