{α : Type u_1} →
  (g : Equiv.Perm α) →
    (motive : (l : List α) → (∀ {x : α}, g x ≠ x → x ∈ l) → Sort u_2) →
      (l : List α) →
        (hg : ∀ {x : α}, g x ≠ x → x ∈ l) →
          ((hg : ∀ {x : α}, g x ≠ x → x ∈ []) → motive [] hg) →
            ((x : α) → (l : List α) → (hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l) → motive (x :: l) hg) → motive l hg