proposition: Lemma simulation_infseq: forall c1 c2, infseq step1 c1 -> inv c1 c2 -> infseq step2 c2.
proof: Proof. intros. apply infseq_coinduction_principle with (X := fun c2 => exists c1, infseq step1 c1 /\ inv c1 c2). - clear c1 c2 H H0. intros c2 (c1 & INF & INV). destruct (simulation_infseq_productive (measure c1 + 1) c1 c2) as (c1' & c2' & PLUS2 & INF' & INV'). lia. auto. auto. exists c2'; split. auto. exists c1'; auto. - exists c1; auto. Qed.
imports: Coq(Psatz) CDF(Sequences)