∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1} (f : F ⟶ G),
  CategoryTheory.IsIso f ↔ CategoryTheory.IsIso (f.app 0) ∧ CategoryTheory.IsIso (f.app 1)