proposition: Lemma from_q1 : forall t:LList acts, Trace A1 q1 t -> exists t' : LList acts, Trace A1 q2 t' /\ t = 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. exists l; auto. + contradiction. Qed.
imports: Arith List RelationClasses