swap (a,b) = (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b)))) by SCMFSA6C:def 3;
hence swap (a,b) is good ; :: thesis: verum