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