proposition: Lemma simulation_star: forall c1 c1', star step1 c1 c1' -> forall c2, inv c1 c2 -> exists c2', star step2 c2 c2' /\ inv c1' c2'.
proof: Proof. induction 1; intros. - exists c2; split. apply star_refl. auto. - destruct (simulation _ _ H _ H1) as (c2' & P & Q). destruct (IHstar _ Q) as (c2'' & U & V). exists c2''; split. eapply star_trans; eauto. destruct P. apply plus_star; auto. destruct H2; auto. auto. Qed.
imports: Coq(Psatz) CDF(Sequences)