theorem Taileqd (_G: wff) (_S1 _S2: set): $ _G -> _S1 == _S2 $ > $ _G -> Tail _S1 == Tail _S2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd | _G -> suc n = suc n |
|
2 | hyp _Sh | _G -> _S1 == _S2 |
|
3 | 1, 2 | eleqd | _G -> (suc n e. _S1 <-> suc n e. _S2) |
4 | 3 | abeqd | _G -> {n | suc n e. _S1} == {n | suc n e. _S2} |
5 | 4 | conv Tail | _G -> Tail _S1 == Tail _S2 |