Inclusion introduction, a lemma derived from incl_equi.
Proof incl_intro. ⊢ (∀x. x ∈ A → x ∈ B) → A ⊆ B, bij_elimr incl_equi.