Theorem incl_from_eq

Proof
01. 1 ⊢ A = B, hypo.
02. ⊢ A ⊆ A, incl_refl.
03. 1 ⊢ A ⊆ B, eq_subst 1 2, P X ↔ A ⊆ X.
incl_from_eq. ⊢ A = B → A ⊆ B, subj_intro 3.

Dependencies
The given proof depends on one axiom:
eq_subst.