fact: Definition swap_xy_2 := ASSIGN "x" (PLUS (VAR "x") (VAR "y")) ;; ASSIGN "y" (MINUS (VAR "x") (VAR "y")) ;; ASSIGN "x" (MINUS (VAR "x") (VAR "y")).
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)