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