(motive : Mathlib.Tactic.ITauto.IProp → Sort u_1) →
  (x : Mathlib.Tactic.ITauto.IProp) →
    ((a : ℕ) → motive (Mathlib.Tactic.ITauto.IProp.var a)) →
      (Unit → motive Mathlib.Tactic.ITauto.IProp.true) →
        (Unit → motive Mathlib.Tactic.ITauto.IProp.false) →
          ((a : Mathlib.Tactic.ITauto.AndKind) →
              (a_1 a_2 : Mathlib.Tactic.ITauto.IProp) → motive (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2)) →
            ((a a_1 : Mathlib.Tactic.ITauto.IProp) → motive (a.or a_1)) →
              ((a a_1 : Mathlib.Tactic.ITauto.IProp) → motive (a.imp a_1)) → motive x