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