The rule subj_intro applied twice consecutively. This admissible rule was added for ergonomic reasons, because it cannot be expressed and derived as a theorem.