proposition: Lemma ProgOk_Remove_Skip_L : forall {av} ext (t1 t2: Telescope av) env prog, {{ t1 }} (Seq Skip prog) {{ t2 }} ∪ {{ ext }} // env -> {{ t1 }} prog {{ t2 }} ∪ {{ ext }} // env.
proof: Proof. SameValues_Facade_t. learn (RunsToSkip env (Equal_refl initial_state)); eauto. learn (RunsToSeq (RunsToSkip _ (Equal_refl _)) H1); eauto. Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.TelAppend