%all(B,all(C,all(D,(B=C and equal_set(B,D)=>equal_set(C,D))))).
input_formula(equal_set_substitution_2,axiom,(
    ! [A,B,C] : 
      ( ( equal(A,B)
        & equal_set(C,A) )
     => equal_set(C,B) )   )).