(def-constant max%on%set 
    "lambda(s:sets[ind_1],f:[ind_1,rr],
          iota(r:rr, 
              forsome(x:ind_1, x in s and r = f(x))
                and
              forall(x:ind_1, x in s implies (not(#(f(x))) or f(x) <= r))))"
    (theory generic-theory-1))

(def-theorem max%on%set-bigger-than-members 
    "forall(s:sets[ind_1],f:[ind_1,rr],x:ind_1,
          x in s 
            and
          #(f(x))
            and
          #(max%on%set(s,f))
            implies 
          f(x) <= max%on%set(s,f))"
    (theory generic-theory-1)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (incorporate-antecedent 
          "with(f:[ind_1,rr],s:sets[ind_1],#(max%on%set(s,f)));")
        (unfold-single-defined-constant-globally max%on%set)
        direct-inference
        (eliminate-defined-iota-expression 0 w)
        (backchain "with(p:prop,p and p);")
        direct-inference
        )))

(def-theorem disj-commutativity 
    "forall(a,b:sets[uu], a disj b iff b disj a)"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        insistent-direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(b,a:sets[uu],a disj b);" ("x"))
        (instantiate-universal-antecedent "with(a,b:sets[uu],b disj a);" ("x"))
        )))

(def-theorem union-disjointness-left 
    "forall(a,b,c:sets[uu], 
          (a union b) disj c 
            iff
          (a disj c and b disj c))"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (block 
            (script-comment 
              "`direct-and-antecedent-inference-strategy' at (0 0)")
            insistent-direct-inference
            (instantiate-universal-antecedent "with(p:prop,p);" ("x"))
            simplify
            simplify)
        (block 
            (script-comment 
              "`direct-and-antecedent-inference-strategy' at (0 1)")
            insistent-direct-inference
            (instantiate-universal-antecedent 
              "with(p:prop,forall(x_$0:uu,p and p or not(p)));"
              ("x"))
            simplify
            simplify)
        (instantiate-universal-antecedent 
          "with(c,a:sets[uu],a disj c);" ("x_$0"))
        (instantiate-universal-antecedent 
          "with(c,b:sets[uu],b disj c);" ("x_$0"))
        )))

(def-theorem union-disjointness-right 
    "forall(a,b,c:sets[uu], 
          a disj (b union c) 
            iff
          (a disj b and a disj c))"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        (force-substitution "a disj b union c" "(b union c) disj a" (0))
        (block 
            (script-comment "`force-substitution' at (0)")
            (apply-macete-with-minor-premises union-disjointness-left)
            (apply-macete-locally 
              disj-commutativity (0) "(b disj a and c disj a)"))
        (block 
            (script-comment "`force-substitution' at (1)")
            (move-to-ancestor 1)
            (apply-macete-locally 
              disj-commutativity (0) "a disj b union c"))
        )))