(def-theorem empty_indic-is-empty 
    "empty_indic_q{empty_indic{uu}}"
    (theory indicators)
    (usages transportable transportable-rewrite)
    (proof (simplify-insistently)))

(def-theorem equals-empty-indic-iff-empty 
    "forall(a:sets[uu], a=empty_indic{uu} iff empty_indic_q{a})"
    reverse
    (theory indicators)
    (usages transportable transportable-rewrite)
    (proof 
      (
        direct-and-antecedent-inference-strategy
        (backchain "with(a:sets[uu],a=empty_indic{uu})")
        (apply-macete-with-minor-premises empty_indic-is-empty)
        extensionality
        beta-reduce-repeatedly
        )))

(def-theorem union-commutativity  
    "forall(a,b:sets[uu], (a union b) = (b union a))"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        extensionality
        direct-inference
        simplify-insistently
        (case-split-on-conditionals (0))
        )))

(def-theorem intersection-commutativity  
    "forall(a,b:sets[uu], (a inters b) = (b inters a))"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        extensionality
        direct-inference
        simplify-insistently
        (case-split-on-conditionals (0))
        simplify
        (contrapose "with(p:prop, p)")
        simplify
        )))    

(def-theorem membership-in-union 
    "forall(x:uu,a,b:sets[uu], x in (a union b) iff (x in a or x in b))"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem membership-in-intersection 
    "forall(x:uu,a,b:sets[uu], x in (a inters b) iff (x in a and x in b))"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem diff-union-equal-whole 
    "forall(x:uu,a,b:sets[uu], b subseteq a implies (a diff b) union b = a)"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        extensionality
        direct-inference
        simplify
        (instantiate-universal-antecedent "with(p:prop,p);" ("x_0"))
        (block 
            (script-comment "node added by `instantiate-universal-antecedent' at (0 0 0)")
            direct-and-antecedent-inference-strategy
            simplify)
        (block 
            (script-comment "node added by `instantiate-universal-antecedent' at (0 0 1)")
            direct-and-antecedent-inference-strategy
            simplify)
        )))

(def-theorem element-of-a-subset-is-an-element 		;  
    "forall(x:uu,b:sets[uu], 
          forsome(a:sets[uu], (x in a) and (a subseteq b))
              implies 
          (x in b))"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent 
          "with(b,a:sets[uu],a subseteq b)" 
          ("x"))
        )))

(def-theorem subseteq-reflexivity 
    "forall(a:sets[uu], a subseteq a)"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem subseteq-antisymmetry 
    "forall(a,b:sets[uu],  a=b iff ((a subseteq b) and (b subseteq a)))"
    (theory indicators)
    (usages transportable-macete)
    (proof; 38 nodes
      (
        insistent-direct-inference-strategy
        (force-substitution "b" "a" (0))
        (force-substitution "a" "b" (0))
        extensionality
        direct-inference
        (antecedent-inference "with(b,a:sets[uu],a subseteq b and b subseteq a)")
        (instantiate-universal-antecedent "with(a,b:sets[uu],b subseteq a)" ("x_0"))
        (instantiate-universal-antecedent "with(b,a:sets[uu],a subseteq b)" ("x_0"))
        simplify
        (instantiate-universal-antecedent "with(b,a:sets[uu],a subseteq b)" ("x_0"))
        simplify
        )))

(def-theorem subseteq-transitivity  
    "forall(a,b,c:sets[uu], 
          (a subseteq b) and (b subseteq c) implies (a subseteq c))"
    (theory indicators)
    (usages transportable-macete)
    (proof 
      (
        insistent-direct-inference-strategy 
        simplify-insistently
        )))

(def-theorem union-disjunction-conversion  
    "forall(x:uu, a,b:sets[uu], (x in (a union b)) iff (x in a or x in b))"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))
  

(def-theorem intersection-conjunction-conversion  
    "forall(x:uu, a,b:sets[uu], (x in (a inters b)) iff (x in a and x in b))"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem singleton-equality-conversion  
    "forall(x,a:uu,x in singleton{a} iff x=a)"
    (theory indicators)
    (usages transportable-rewrite transportable-macete)
    (proof (simplify-insistently)))
  

(def-theorem difference-conjunction-conversion  
    "forall(x:uu, a,b:sets[uu], (x in (a diff b)) iff (x in a and not (x in b)))"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently))) 

(def-compound-macete indicator-conversions 
    (repeat 
      tr%union-disjunction-conversion
      tr%intersection-conjunction-conversion
      tr%singleton-equality-conversion
      tr%difference-conjunction-conversion))

(def-theorem big-union-member 
    "forall(f:[index,sets[uu]],x:uu, 
          x in big_u{f} iff forsome(i:index,x in f(i)))"
    (theory family-indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem big-intersection-member 
    "forall(f:[index,sets[uu]],
          x:uu, x in big_i{f} iff forall(i:index,x in f(i)))"
    (theory family-indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))
    

(def-theorem in-singleton-iff-equals-single-member 
    "forall(x,y:uu, x in singleton{y} iff x=y)"
    reverse
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem singletons-have-a-unique-member 
    "forall(a:sets[uu],y:uu, a=singleton{y} iff y=iota(x:uu, x in a))"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises eliminate-iota-macete)
        direct-and-antecedent-inference-strategy
        (force-substitution "a" "singleton{y}" (0))
        beta-reduce-insistently
        (contrapose "with(y:uu,a:sets[uu],a=singleton{y})")
        extensionality
        (instantiate-existential ("b_$0"))
        simplify
        (force-substitution "y" "iota(x:uu,x in a)" (0))
        (eliminate-defined-iota-expression 0 u)
        extensionality
        direct-inference
        (instantiate-universal-antecedent "with(p:prop, forall(u_1:uu,p))" ("x_0"))
        simplify
        (raise-conditional (0))
        direct-and-antecedent-inference-strategy
        (simplify-antecedent "with(x_0:uu,a:sets[uu],not(x_0 in a))")
        simplify
        )))

(def-theorem diff-with-indic-is-disj-from-indic 
    "forall(a,b:sets[uu],  (a diff b) disj b)"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem membership-in-diff 
    "forall(x:uu,a,b:sets[uu], (x in a diff b) iff (x in a and not(x in b)))"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem decremented-partition-lemma 
    "forall(w:sets[sets[uu]],a,b:sets[uu], 
          partition_q{w,a} and b in w implies 
          partition_q{w diff singleton{b},a diff b})"
    (theory indicators)
    (usages transportable-macete)
    (proof; 74 nodes
      (
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent 
          "with(p:prop, forall(u,v:sets[uu],p))" ("u_$0" "v_$0"))
        (contrapose "with(p:prop, not(p))")
        (weaken (0 1 3 4 5))
        (incorporate-antecedent "with(p:prop, p)")
        simplify-insistently
        (contrapose "with(p:prop, not(p))")
        (weaken (0 2 3 4 5))
        (incorporate-antecedent "with(p:prop, p)")
        simplify-insistently
        (weaken (0))
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent 
          "with(p:prop, forall(x:uu,p))" ("x_$0"))
        (instantiate-existential ("u"))
        extensionality
        (instantiate-existential ("x_$0"))
        simplify
        (backchain "with(p:prop, forall(x:uu,p))")
        (instantiate-existential ("u_$0"))
        (instantiate-universal-antecedent 
          "with(p:prop, forall(u,v:sets[uu],p))" ("u_$0" "b"))
        (weaken (2 3 4 5 6))
        (incorporate-antecedent "with(p:prop, p)")
        simplify-insistently
        )))
    

(def-theorem union-of-a-difference 
    "forall(a,b:sets[uu], a subseteq b implies a union (b diff a) = b)"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises subseteq-antisymmetry)
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (backchain "with(b,a:sets[uu],a subseteq b);")
        )))

(def-theorem difference-of-a-disjoint-union 
    "forall(a,b:sets[uu], a inters b=empty_indic{uu} implies (a union b) diff a = b)"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        (prove-by-logic-and-simplification 0)
        (block
            (script-comment
              "node added by `prove-by-logic-and-simplification' at (0 0 0 (1 . 0)
0 0 0 0 (1 . 1) (1 . 0) 1 0)")
            (contrapose "with(f:sets[uu],f=f);")
            simplify-insistently
            extensionality
            (instantiate-existential ("x_0"))
            simplify)
        (contrapose "with(f:sets[uu],f=f);"))))

(def-theorem difference-of-disjoint-sets 
    "forall(a,b:sets[uu], a inters b=empty_indic{uu} implies a diff b = a)"
    (theory indicators)
    (usages transportable-macete)
    (proof 
      (
        simplify-insistently
        (prove-by-logic-and-simplification 0)
        (contrapose "with(f:sets[uu],f=f);")
        (prove-by-logic-and-simplification 0)
        auto-instantiate-existential)))

(def-theorem difference-of-a-union 
    "forall(a,b:sets[uu], (a union b) diff a = b diff a)"
    (theory indicators)
    (usages transportable-macete)
    (proof
      (
        (prove-by-logic-and-simplification 0))))

(def-theorem union-with-empty 
    "forall(a:sets[uu], (a union empty_indic{uu}) = a)"
    (theory indicators)
    (usages transportable-macete)
    (proof
      ((prove-by-logic-and-simplification 0))))