(def-theorem big-union-recursion
*"forall(f:[index,sets[uu]], i:index,
i in dom{f}
implies
big_u{f} = f(i) union big_u{lambda(k:index, if(not(k=i), f(k),?sets[uu]))})"*
(theory family-indicators)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(block
(script-comment *"`direct-and-antecedent-inference-strategy' at (0)"*)
insistent-direct-inference
(apply-macete-with-minor-premises union-disjunction-conversion)
(apply-macete-with-minor-premises big-union-member)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-existential (*"i_$0"*))
(cut-with-single-formula *"not(i_$0=i)"*)
simplify
(block
(script-comment *"`cut-with-single-formula' at (1)"*)
(contrapose *"with(p:prop,not(p));"*)
simplify))
(block
(script-comment *"`direct-and-antecedent-inference-strategy' at (1)"*)
insistent-direct-inference
(apply-macete-with-minor-premises union-disjunction-conversion)
(apply-macete-with-minor-premises big-union-member)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
auto-instantiate-existential
(block
(script-comment *"`direct-and-antecedent-inference-strategy' at (0 1 0)"*)
(instantiate-existential (*"i_$0"*))
(cut-with-single-formula *"not(i_$0=i)"*)
(contrapose *"with(x_$0:uu,f:sets[uu],x_$0 in f);"*)
simplify))
)))

(def-theorem union-special-case
*"forall(f:[index,sets[uu]], j,k:index,
dom{f}=indic{i:index, i=j or i=k}
implies
big_u{f} = f(j) union f(k))"*
(theory family-indicators)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
extensionality
simplify
direct-and-antecedent-inference-strategy
(cut-with-single-formula *"i in dom{f}"*)
(move-to-sibling 1)
simplify
(block
(script-comment *"node added by `cut-with-single-formula' at (0)"*)
(contrapose *"with(i:index,f:sets[index],i in f);"*)
(backchain *"with(f:sets[index],f=f);"*)
(apply-macete-with-minor-premises indicator-facts-macete)
simplify
(contrapose *"with(x_0:uu,k:index,f:[index,sets[uu]],not(x_0 in f(k)));"*)
(antecedent-inference *"with(p:prop,p implies p);"*)
(simplify-antecedent *"with(p:prop,not(p));"*)
simplify)
)))