 Now making use of the hypothesis that ⊢ is →-introductive—which does not follow from the fact that ⊢I L is →-introductive and ⊢ ⊇ ⊢I L—the first condition now allows for successive rewriting, first as