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