∀ {index? lowlink? : Option ℕ} {onStack : Bool} {index?_1 lowlink?_1 : Option ℕ} {onStack_1 : Bool},
  { index? := index?, lowlink? := lowlink?, onStack := onStack } =
      { index? := index?_1, lowlink? := lowlink?_1, onStack := onStack_1 } →
    index? = index?_1 ∧ lowlink? = lowlink?_1 ∧ onStack = onStack_1