[Merged by Bors] - feat: align init.{core, logic}

[digama0]

With this, the files init.core and init.logic are synchronized, although we aren't currently tracking files from init in port-status.

[semorrison]

bors merge

[bors]

Build failed:

• Build

[semorrison]

This did not compile with master. I merged, and fixed the imports in Simps.

In Init.Logic, the new @[trans] attribute PR'd in #253 incorrectly rejected the @[trans] attribute on

@[deprecated, trans] theorem Implies.trans {p q r : Prop} (h₁ : p → q) (h₂ : q → r) :
    p → r := fun hp => h₂ (h₁ hp)

I left a note and removed the attribute for now.

[digama0]

The original lean 3 would have rejected it too - I rewrote the theorem to use -> instead of Implies, but I guess that's not an option in this case. trans will probably need special support to handle ->.

[digama0]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style