proposition: Lemma swap_xy_correct: forall s, exists s', star red (swap_xy, s) (SKIP, s') /\ s' "x" = s "y" /\ s' "y" = s "x".
proof: Proof. intros. econstructor; split. - eapply star_step. apply red_seq_step. apply red_assign. eapply star_step. apply red_seq_done. eapply star_step. apply red_seq_step. apply red_assign. eapply star_step. apply red_seq_done. eapply star_step. apply red_assign. apply star_refl. - unfold update; cbn. auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)