proposition: Lemma from_q2 : forall t:LList acts, Trace A1 q2 t -> exists t' : LList acts, (Trace A1 q2 t' \/ Trace A1 q1 t') /\ t = LCons b t'.
proof: Proof. intros t H; inversion_clear H. - case (no_deadlocks H0). - generalize H0 H1; case a0; cbn in |- *. + contradiction. + do 2 simple destruct 1. * exists l; auto. * exists l; auto. rewrite H3; auto. * contradiction. Qed.
imports: Arith List RelationClasses