(def-quasi-constructor equinumerous 
    "lambda(a:sets[ind_1],b:sets[ind_2], 
          forsome(f:[ind_1,ind_2], bijective_on_q(f,a,b)))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor embeds 
    "lambda(a:sets[ind_1],b:sets[ind_2], 
          forsome(f:[ind_1,ind_2],
              dom(f)=a and (ran(f) subseteq b) and injective_on_q(f,a)))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-theorem equinumerous-is-reflexive 
    "forall(a:sets[ind_1], a equinumerous a)"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof; 10 nodes
      (
        direct-inference
        (instantiate-existential ("id{a}"))
        insistent-direct-inference
        insistent-direct-inference
        (apply-macete-with-minor-premises dom-of-id)
        (apply-macete-with-minor-premises ran-of-id)
        (apply-macete-with-minor-premises id-is-injective-on-dom)
        )))

(def-theorem equinumerous-is-symmetric 
    "forall(a:sets[ind_1],b:sets[ind_2], 
          (a equinumerous b) implies (b equinumerous a))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("inverse{f}"))
        insistent-direct-inference-strategy
        (apply-macete-with-minor-premises dom-of-inverse)
        (apply-macete-with-minor-premises injective-iff-injective-on-domain)
        simplify
        (apply-macete-with-minor-premises ran-of-inverse)
        (instantiate-theorem inverse-is-injective ("f"))
        (backchain "with(f:[ind_1,ind_2],injective_q{inverse{f}})")
        )))

(def-theorem equinumerous-is-transitive 
    "forall(a:sets[ind_1],b:sets[ind_2],c:sets[ind_3],
          (a equinumerous b) and (b equinumerous c) implies (a equinumerous c))"
    (theory pure-generic-theory-3)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("f_$0 oo f"))
        insistent-direct-inference-strategy
        (apply-macete-with-minor-premises domain-composition)
        (apply-macete-with-minor-premises range-composition)
        (cut-with-single-formula "injective_q{f}")
        (cut-with-single-formula "injective_q{f_$0 oo f}")
        (backchain 
          "with(f:[ind_1,ind_2],f_$0:[ind_2,ind_3], injective_q{f_$0 oo f})")
        (apply-macete-with-minor-premises injective-composition)
        simplify
        (apply-macete-with-minor-premises injective-iff-injective-on-domain)
        simplify
        )))

(def-theorem equals-implies-equinumerous 
    "forall(a,b:sets[ind_1], a=b implies a equinumerous b)"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop, p)")
        (apply-macete-with-minor-premises equinumerous-is-reflexive)
        )))

(def-theorem embeds-is-reflexive 
    "forall(a:sets[ind_1], a embeds a)"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        (instantiate-existential ("id{a}"))
        (apply-macete-with-minor-premises dom-of-id)
        (apply-macete-with-minor-premises ran-of-id)
        (apply-macete-with-minor-premises id-is-injective-on-dom)
        )))

(def-theorem embeds-is-transitive 
    "forall(a:sets[ind_1],b:sets[ind_2],c:sets[ind_3],
          (a embeds b) and (b embeds c) implies (a embeds c))"
    (theory pure-generic-theory-3)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("f_$1 oo f_$0"))
        (apply-macete-with-minor-premises domain-composition)
        (apply-macete-with-minor-premises tr%subseteq-transitivity)
        auto-instantiate-existential
        (apply-macete-with-minor-premises composition-decreases-range)
        (apply-macete-with-minor-premises tr%injective-implies-injective-on)
        (apply-macete-with-minor-premises injective-composition)
        (apply-macete-with-minor-premises injective-iff-injective-on-domain)
        direct-inference
        (weaken (0 1 3 5 6 7))
        simplify
        (weaken (0 1 2 3 5 6 7))
        insistent-direct-inference-strategy
        simplify
        )))

(def-theorem equinumerous-implies-embeds 
    "forall(a:sets[ind_1],b:sets[ind_2], 
          (a equinumerous b) implies (a embeds b))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        auto-instantiate-existential
        (incorporate-antecedent "with(b:sets[ind_2],f:[ind_1,ind_2],ran{f}=b)")
        (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
        simplify
        )))

(def-theorem embeds-implies-equinumerous-to-subset 
    "forall(a:sets[ind_1],b:sets[ind_2], 
          (a embeds b) 
            implies 
          forsome(c:sets[ind_2], a equinumerous c and c subseteq b))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("ran{f_$1}"))
        (instantiate-existential ("f_$1"))
        insistent-direct-inference
        )))

(def-theorem equinumerous-embeds-transitivity 
    "forall(a:sets[ind_1],b:sets[ind_2],c:sets[ind_3],
          (a equinumerous b) and (b embeds c) implies (a embeds c))"
    (theory pure-generic-theory-3)
    (usages transportable-macete)
    (proof
      (
        direct-inference-strategy
        (apply-macete-with-minor-premises embeds-is-transitive)
        (instantiate-existential ("b"))
        (apply-macete-with-minor-premises equinumerous-implies-embeds)
        )))
    

(def-theorem embeds-equinumerous-transitivity 
    "forall(a:sets[ind_1],b:sets[ind_2],c:sets[ind_3],
          (a embeds b) and (b equinumerous c) implies (a embeds c))"
    (theory pure-generic-theory-3)
    (usages transportable-macete)
    (proof
      (
        direct-inference-strategy
        (apply-macete-with-minor-premises embeds-is-transitive)
        (instantiate-existential ("b"))
        (apply-macete-with-minor-premises tr%equinumerous-implies-embeds)
        )))

(def-theorem embeds-in-empty-indic 
    "forall(a:sets[ind_1],
          (a embeds empty_indic{ind_2}) iff a=empty_indic{ind_1})"
    reverse
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (force-substitution "a" "dom{f_$1}" (0))
        extensionality
        direct-inference
        simplify
        (contrapose "with(a,b:sets[ind_2], a subseteq b)")
        (instantiate-existential ("f_$1(x_0)"))
        (apply-macete-with-minor-premises range-domain-membership)
        (apply-macete-with-minor-premises domain-membership-iff-defined)
        simplify-insistently
        simplify
        (force-substitution "a" "empty_indic{ind_1}" (0))
        (weaken (0))
        (instantiate-existential ("lambda(x:ind_1,?ind_2)"))
        extensionality
        direct-inference
        simplify
        insistent-direct-inference-strategy
        simplify-insistently
        insistent-direct-inference-strategy
        (antecedent-inference "with(p,q,r:prop, p and q and r)")
        (contrapose "with(x_$6:ind_1,x_$6 in empty_indic{ind_1})")
        simplify-insistently
        )))

(def-theorem equinumerous-to-empty-indic 
    "forall(a:sets[ind_1],
          (a equinumerous empty_indic{ind_2}) iff a=empty_indic{ind_1})"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-inference-strategy
        (apply-macete-with-minor-premises rev%embeds-in-empty-indic)
        (apply-macete-with-minor-premises equinumerous-implies-embeds)
        (force-substitution "a" "empty_indic{ind_1}" (0))
        (instantiate-existential ("lambda(x:ind_1,?ind_2)"))
        insistent-direct-inference-strategy
        extensionality
        direct-inference
        simplify
        extensionality
        direct-inference
        simplify
        simplify
        (beta-reduce-antecedent "with(p,q,r:prop, p and q and r)")
        )))

(def-theorem subset-embeds-in-superset 
    "forall(a,b:sets[ind_1],
          (a subseteq b) implies (a embeds b))"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("id{a}"))
        (apply-macete-with-minor-premises dom-of-id)
        (apply-macete-with-minor-premises ran-of-id)
        (apply-macete-with-minor-premises id-is-injective-on-dom)
        )))