proposition: Lemma simulation_cont_red: forall C1 C1', step C1 C1' -> forall C2, match_conf C1 C2 -> exists C2', (plus red C2 C2' \/ (star red C2 C2' /\ kmeasure C1' < kmeasure C1))%nat /\ match_conf C1' C2'.
proof: Proof. destruct 1; intros C2 MC; inversion MC; subst; cbn. 2: econstructor; split; [right; split; [apply star_refl | lia] | constructor; auto ]. 1-6: econstructor; split; [left; apply plus_one; apply red_apply_cont; auto using red | constructor; auto]. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)