(def-theorem defined-iota-expression 
    "forall(p:[ind_1,prop], 
          #(iota(i:ind_1,p(i))) 
              implies
          (p(iota(i:ind_1,p(i))) and 
          forall(j:ind_1, p(j) implies j=iota(i:ind_1,p(i)))))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        direct-inference
        (cut-with-single-formula 
          "#(iota(i:ind_1,p(i))) and forall(x:ind_1,x=x)")
        (contrapose "with(i:ind_1,#(i));")
        (eliminate-iota 0)
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:prop,p or p);")
        direct-inference
        (block 
            (script-comment "`direct-inference' at (0)")
            (eliminate-iota 0)
            (instantiate-existential ("y%iota")))
        (block 
            (script-comment "`direct-inference' at (1)")
            (instantiate-universal-antecedent-multiply 
              "with(y%iota:ind_1,p:[ind_1,prop],
                  forall(z%iota:ind_1,p(z%iota) implies z%iota=y%iota));"
              (("j") ("iota(i:ind_1,p(i))")))
            direct-inference
            direct-inference)
        )))

(def-theorem defined-iota-expression-satisfiability 
    "forall(p:[ind_1,prop], 
          #(iota(i:ind_1,p(i))) implies p(iota(i:ind_1,p(i))))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem defined-iota-expression ("p"))
        )))

(def-theorem defined-iota-expression-existence 
    "forall(p:[ind_1,prop], 
          #(iota(i:ind_1,p(i))) implies nonvacuous_q{p})"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem defined-iota-expression ("p"))
        auto-instantiate-existential
        )))

(def-theorem defined-iota-expression-full-existence 
    "forall(%%p%%:[ind_1,prop], 
          not(#(iota(i:ind_1,%%p%%(i)))) 
            or
          forsome(j:ind_1, 
              j=iota(i:ind_1,%%p%%(i)) and %%p%%(j) and forall(j_1:ind_1, %%p%%(j_1) 
                implies 
              j=j_1)))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem defined-iota-expression ("%%p%%"))
        auto-instantiate-existential
        (instantiate-universal-antecedent 
          "with(%%p%%:prop, forall(j:ind_1,%%p%%))" ("j_$0"))
        )))

(def-theorem defined-iota-expression-uniqueness 
    "forall(p:[ind_1,prop], 
          #(iota(i:ind_1,p(i))) 
                implies
          forall(j:ind_1, p(j) implies j=iota(i:ind_1,p(i))))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem defined-iota-expression ("p"))
        (backchain "with(p,q:prop, forall(j:ind_1, p implies q))")
        )))

(def-theorem defined-iota-expression-iota-free-uniqueness 
    "forall(p:[ind_1,prop], 
          #(iota(i:ind_1,p(i))) 
              implies
          forall(i,j:ind_1, (p(i) and p(j)) implies i=j))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem defined-iota-expression ("p"))
        (instantiate-universal-antecedent-multiply 
          "with(p:prop,forall(j:ind_1,p));"
          (("i") ("j")))
        )))

(def-theorem equal-iota-expressions-lemma 
    "forall(p,q:[ind_1,prop], 
          iota(i:ind_1,p(i)) = iota(i:ind_1,q(i)) 
              implies
          forall(k:ind_1, p(k) implies q(k)))"
    lemma
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem defined-iota-expression-uniqueness ("p"))
        (instantiate-universal-antecedent "with(p:prop, forall(j:ind_1,p))" ("k"))
        (force-substitution "k" "iota(i:ind_1,q(i))" (0))
        (apply-macete-with-minor-premises defined-iota-expression-satisfiability)
        )))

(def-theorem equal-iota-expressions 
    "forall(p,q:[ind_1,prop], 
          iota(i:ind_1,p(i)) = iota(i:ind_1,q(i)) implies p=q)"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        extensionality
        direct-inference
        simplify
        (instantiate-theorem equal-iota-expressions-lemma ("p" "q"))
        (instantiate-theorem equal-iota-expressions-lemma ("q" "p"))
        (instantiate-universal-antecedent 
          "with(p,q:[ind_1,prop],forall(k:ind_1,q(k) implies p(k)));" ("x_0"))
        (instantiate-universal-antecedent 
          "with(q,p:[ind_1,prop],forall(k:ind_1,p(k) implies q(k)));" ("x_0"))
        simplify
        simplify
        )))

(def-theorem defined-iota-expression-elimination 
    "forall(p:[ind_1,prop], 
          #(iota(i:ind_1,p(i))) 
              iff 
          forsome(i:ind_1, p(i) and forall(j:ind_1, p(j) implies j=i)))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem defined-iota-expression-full-existence ("p"))
        (instantiate-existential ("j"))
        (instantiate-universal-antecedent 
          "with(p:prop, forall(j_1:ind_1,p))" ("j_$0"))
        (eliminate-iota 0)
        auto-instantiate-existential
        direct-and-antecedent-inference-strategy
        (instantiate-theorem defined-iota-expression-full-existence ("p"))
        (instantiate-existential ("j"))
        (instantiate-universal-antecedent 
          "with(p:prop, forall(j_1:ind_1,p))" ("j_$0"))
        )))

(def-theorem negated-defined-iota-expression-elimination-1 
    "forall(p:[ind_1,prop], 
          forall(i:ind_1, not(p(i))) 
            implies 
          not(#(iota(i:ind_1,p(i)))))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (eliminate-iota 0)
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:[ind_1,prop],forall(i:ind_1,not(p(i))));")
        auto-instantiate-existential
        )))

(def-theorem negated-defined-iota-expression-elimination-2 
    "forall(p:[ind_1,prop], 
          forsome(i,j:ind_1, p(i) and p(j) and not(i=j))
            implies 
          not(#(iota(i:ind_1,p(i)))))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (eliminate-iota 0)
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:prop,not(p));")
        (instantiate-universal-antecedent-multiply 
          "with(y%iota:ind_1,p:[ind_1,prop],
                forall(z%iota:ind_1,p(z%iota) implies z%iota=y%iota));"
          (("i") ("j")))
        )))

(def-theorem negated-defined-iota-expression-elimination 
    "forall(p:[ind_1,prop], 
          not(#(iota(i:ind_1,p(i)))) 
              iff 
          (forall(i:ind_1, 
                not(p(i))) 
                  or 
                forsome(i,j:ind_1, p(i) and p(j) and not(i=j))))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:[ind_1,prop],not(#(iota(i:ind_1,p(i)))));")
        (eliminate-iota 0)
        auto-instantiate-existential
        (backchain "with(p:prop, forall(i,j:ind_1,p))")
        simplify
        (apply-macete-with-minor-premises 
          negated-defined-iota-expression-elimination-1)
        (apply-macete-with-minor-premises 
          negated-defined-iota-expression-elimination-2)
        auto-instantiate-existential
        )))

(def-theorem left-iota-expression-equation-elimination 
    "forall(a:ind_1,p:[ind_1,prop], 
          iota(i:ind_1,p(i)) = a iff (p(a) and forall(b:ind_1, p(b) implies b=a)))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (force-substitution "a" "iota(i:ind_1,p(i))" (0))
        (apply-macete-with-minor-premises 
          defined-iota-expression-satisfiability)
        (apply-macete-with-minor-premises 
          defined-iota-expression-iota-free-uniqueness)
        auto-instantiate-existential
        (eliminate-iota 0)
        auto-instantiate-existential
        )))

(def-theorem right-iota-expression-equation-elimination 
    "forall(a:ind_1,p:[ind_1,prop], 
          a = iota(i:ind_1,p(i)) iff (p(a) and forall(b:ind_1, p(b) implies b=a)))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (force-substitution "a" "iota(i:ind_1,p(i))" (0))
        (apply-macete-with-minor-premises 
          defined-iota-expression-satisfiability)
        (apply-macete-with-minor-premises 
          defined-iota-expression-iota-free-uniqueness)
        auto-instantiate-existential
        (eliminate-iota 0)
        auto-instantiate-existential
        )))

(def-schematic-macete tr%abstraction-for-iota-body
    "with(body:prop, 
          iota(i:ind_1,body) == iota(i:ind_1,lambda(i:ind_1,body)(i)))"
    null
    transportable
    (theory pure-generic-theory-1))

(def-compound-macete iota-abstraction-macete 
    (sound
      tr%abstraction-for-iota-body
      beta-reduce-unstoppably
      beta-reduce-unstoppably))

(def-schematic-macete tr%abstraction-for-forsome-body
    "with(body:prop, 
          forsome(i:ind_1,body) iff forsome(i:ind_1,lambda(i:ind_1,body)(i)))"
    null
    transportable
    (theory pure-generic-theory-1))

(def-compound-macete eliminate-iota-macete 
    (sequential
      iota-abstraction-macete
      (series
        tr%defined-iota-expression-elimination
        tr%negated-defined-iota-expression-elimination
        tr%left-iota-expression-equation-elimination
        tr%right-iota-expression-equation-elimination)
      beta-reduce))

(def-compound-macete eliminate-forsome-macete 
    (sequential
      (sound
        tr%abstraction-for-forsome-body
        beta-reduce-unstoppably
        beta-reduce-unstoppably)
      tr%defined-iota-expression-existence
      beta-reduce))