(def-theorem finiteness-of-subgroups 
    "forall(a:sets[gg], 
          f_indic_q{gg%subgroup} and subgroup(a) implies f_indic_q{a})"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
        (instantiate-existential ("gg%subgroup"))
        (apply-macete-with-minor-premises subgroups-are-subsets-of-gg%subgroup)
        )))

(def-theorem finiteness-of-stabilizers 
    "forall(alpha:uu, 
          f_indic_q{gg%subgroup} implies f_indic_q{stabilizer(alpha)})"
    (theory group-actions)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises finiteness-of-subgroups)
        (apply-macete-with-minor-premises stabilizers-are-subgroups)
        )))
    

(def-theorem right-cosets-are-equinumerous 
    "forall(a:sets[gg],g,h:gg, right%trans(a,g) equinumerous right%trans(a,h))"
    (theory groups)
    (usages transportable-macete)
    (proof
      (; 169 nodes
        direct-inference
        (unfold-single-defined-constant-globally right%trans)
        (instantiate-existential 
          ("lambda(i:gg,iota(j:gg, 
                  forsome(k:gg, (k in a) and i=k mul g and j=k mul h)))"))
        insistent-direct-inference
        (block 
            (script-comment "node added by `insistent-direct-inference' at (0)")
            insistent-direct-inference
            (block 
	(script-comment "node added by `insistent-direct-inference' at (0)")
	extensionality
	direct-inference
	beta-reduce-repeatedly
	simplify
	direct-and-antecedent-inference-strategy
	(block 
	    (script-comment 
	      "node added by `direct-and-antecedent-inference-strategy' at (0)")
	    (contrapose "with(p:prop,p);")
	    (eliminate-iota 0)
	    direct-and-antecedent-inference-strategy
	    (contrapose "with(p:prop,forall(i_$2:gg,p or p));")
	    (instantiate-existential ("k")))
	(block 
	    (script-comment 
	      "node added by `direct-and-antecedent-inference-strategy' at (1 0 0)")
	    (contrapose "with(p:prop,not(p));")
	    (eliminate-iota 0)
	    (instantiate-existential ("i_$2 mul h"))
	    auto-instantiate-existential
	    (block 
	        (script-comment "node added by `instantiate-existential' at (0 1 0 0)")
	        (antecedent-inference-strategy (0))
	        (backchain "with(h,k_$0,z%iota_$0:gg,z%iota_$0=k_$0 mul h);")
	        (apply-macete-with-minor-premises group-cancellation-laws)
	        (force-substitution "k_$0" "x_0 mul inv(g)" (0))
	        (block 
	            (script-comment "node added by `force-substitution' at (0)")
	            (backchain "with(g,i_$2,x_0:gg,x_0=i_$2 mul g);")
	            (weaken (5 4 3 2 1 0))
	            simplify)
	        (block 
	            (script-comment "node added by `force-substitution' at (1)")
	            (weaken (5 4 3 2 0))
	            simplify
	            (backchain "with(p:prop,p);")
	            (weaken (0))
	            simplify))))
            (block 
	(script-comment "node added by `insistent-direct-inference' at (1)")
	(weaken (0))
	extensionality
	direct-inference
	beta-reduce-repeatedly
	simplify
	direct-and-antecedent-inference-strategy
	(block 
	    (script-comment 
	      "node added by `direct-and-antecedent-inference-strategy' at (0 0)")
	    (cut-with-single-formula 
	      "#(iota(j:gg, forsome(k:gg,k in a and x_$10=k mul g and j=k mul h)))")
	    (incorporate-antecedent "with(g,x_0:gg,x_0=g);")
	    (eliminate-defined-iota-expression 0 u)
	    direct-and-antecedent-inference-strategy
	    (antecedent-inference "with(p:prop,forsome(k:gg,p));")
	    (instantiate-existential ("k")))
	(block 
	    (script-comment 
	      "node added by `direct-and-antecedent-inference-strategy' at (1 0 0)")
	    (contrapose "with(p:prop,not(p));")
	    (instantiate-existential ("i_$1 mul g"))
	    (apply-macete-with-minor-premises eliminate-iota-macete)
	    direct-and-antecedent-inference-strategy
	    auto-instantiate-existential
	    (block 
	        (script-comment 
	          "node added by `direct-and-antecedent-inference-strategy' at (1 0 0 0 0 0 0)")
	        (backchain "with(h,k_$1,x_0:gg,x_0=k_$1 mul h);")
	        (backchain "with(h,k_$0,b_$0:gg,b_$0=k_$0 mul h);")
	        (incorporate-antecedent "with(k_$1,g,i_$1:gg,i_$1 mul g=k_$1 mul g);")
	        (incorporate-antecedent "with(k_$0,g,i_$1:gg,i_$1 mul g=k_$0 mul g);")
	        (apply-macete-with-minor-premises group-cancellation-laws)
	        (weaken (5 4 3 2 1 0))
	        simplify))))
        (block 
            (script-comment "node added by `insistent-direct-inference' at (1)")
            (weaken (0))
            insistent-direct-inference
            simplify
            direct-and-antecedent-inference-strategy
            (cut-with-single-formula 
              "#(iota(j:gg, forsome(k:gg,k in a and x_$1=k mul g and j=k mul h)))")
            (cut-with-single-formula 
              "#(iota(j:gg, forsome(k:gg,k in a and x_$2=k mul g and j=k mul h)))")
            (incorporate-antecedent "with(p:prop,iota(j:gg,p)=iota(j:gg,p));")
            (eliminate-defined-iota-expression 0 u)
            (eliminate-defined-iota-expression 0 v)
            (antecedent-inference-strategy (0 2))
            (weaken (2 3 4 5 8 9 10 11 12 13))
            (backchain "with(h,k,v:gg,v=k mul h);")
            (backchain "with(g,k,x_$2:gg,x_$2=k mul g);")
            (backchain "with(g,k_$0,x_$1:gg,x_$1=k_$0 mul g);")
            (backchain "with(h,k_$0,u:gg,u=k_$0 mul h);")
            (apply-macete-with-minor-premises group-cancellation-laws))
        )))