fact: Example Hoare_swap_xy_2: forall m n, Hoare (aequal (VAR "x") m //\\ aequal (VAR "y") n) swap_xy_2 (aequal (VAR "x") n //\\ aequal (VAR "y") m).
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)