(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))))