(def-theorem lct-obligation-1 
    "#(restrict2{mul,b,b},[b%sort,b%sort,b%sort])"
    lemma
    (theory lct-theory)
    (proof
      (
        sort-definedness
        simplify
        (apply-macete-with-minor-premises b%sort-defining-axiom_lct-theory)
        (apply-macete-with-minor-premises lct-macete)
        )))

(def-theorem lct-obligation-2 
    "#(restrict{inv,b},[b%sort,b%sort])"
    lemma
    (theory lct-theory)
    (proof
      (
        sort-definedness
        simplify
        (apply-macete-with-minor-premises b%sort-defining-axiom_lct-theory)
        (apply-macete-with-minor-premises lct-macete)
        )))

(def-theorem lct-obligation-3 
    "#(restrict2{right%trans,a%cosets,b},[a%cosets%sort,b%sort,a%cosets%sort])"
    lemma
    (theory lct-theory)
    (proof
      (
        sort-definedness
        direct-inference
        (case-split ("#(xx_0,sets[gg])"))
        simplify
        (unfold-single-defined-constant-globally a%cosets)
        simplify
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises a%cosets%sort-defining-axiom_lct-theory)
        simplify
        (unfold-single-defined-constant-globally a%cosets)
        simplify
        (backchain "with(g:gg,xx_0:sets[gg],xx_0=right%trans(a,g))")
        (instantiate-existential ("g mul xx_1"))
        (apply-macete-with-minor-premises lct-macete)
        (apply-macete-with-minor-premises simplify-set-translations)
        simplify
        )))

(def-theorem lct-obligation-4 
    "forall(x:b%sort,inv(x) in b)"
    lemma
    (theory lct-theory)
    (proof
      (
        (apply-macete-with-minor-premises lct-macete)
        )))

(def-theorem lct-obligation-5 
    "forall(x,y:b%sort,(x mul y) in b)"
    lemma
    (theory lct-theory)
    (proof
      (
        (apply-macete-with-minor-premises lct-macete)
        )))

(def-theorem lct-obligation-6 
    "forall(g,h:b%sort,(g mul h) in b)
        and 
      (forall(alpha:a%cosets%sort,g:b%sort, right%trans(alpha,g) in a%cosets)
          and 
        forall(alpha:a%cosets%sort,g,h:b%sort,
          right%trans(alpha,g mul h)=right%trans(right%trans(alpha,g),h)))"
    lemma
    (theory lct-theory)
    (proof
      (
        (apply-macete-with-minor-premises lct-macete)
        direct-and-antecedent-inference-strategy
        (block 
          (script-comment 
            "node added by `direct-and-antecedent-inference-strategy' at (0 0)")
          (unfold-single-defined-constant-globally a%cosets)
          simplify
          (cut-with-single-formula "alpha in a%cosets")
          (block 
            (script-comment "node added by `cut-with-single-formula' at (0)")
            (incorporate-antecedent "with(p:prop,p);")
            (unfold-single-defined-constant-globally a%cosets)
            simplify
            direct-and-antecedent-inference-strategy
            (backchain "with(f:sets[gg],alpha:a%cosets%sort,alpha=f);")
            (instantiate-existential ("g_$0 mul g"))
            (block 
              (script-comment "node added by `instantiate-existential' at (0 0)")
              (apply-macete-with-minor-premises lct-macete)
              (apply-macete-with-minor-premises b%sort-members-are-in-b))
            (apply-macete-with-minor-premises simplify-set-translations))
          (apply-macete-with-minor-premises a%cosets%sort-members-are-in-a%cosets))
        (apply-macete-with-minor-premises simplify-set-translations)
        )))