∀ {E : Type u_2} {X : Type u_3} {A : Type u_1} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] (q : E → OpenPartialHomeomorph E X) (t : ℕ → ↑unitInterval) (n : ℕ) (N : Set A)
  (g' : ↑unitInterval × A → E) (e : E) (v : Set A) (ta : ↑unitInterval × A)
  (motive :
    ta ∈ Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun y => (t n, y)) ⁻¹' (q e).source)) ∩ frontier {a | a.1 ≤ t n} →
      Prop)
  (x : ta ∈ Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun y => (t n, y)) ⁻¹' (q e).source)) ∩ frontier {a | a.1 ≤ t n}),
  (∀ (left : ta.1 ∈ Set.Icc 0 (t n.succ)) (hav : ta.2 ∈ v) (left_1 : ta.2 ∈ N)
      (ha : ta.2 ∈ (g' ∘ fun y => (t n, y)) ⁻¹' (q e).source) (hfr : ta ∈ frontier {a | a.1 ≤ t n}), motive ⋯) →
    motive x