
>pub B;C;p = B;C;p;C -> C;(B;p)*;~B = C;(B;p)*;~B;C;~B
>focus
>r d d d r r
>cite commut. l
>r
>unf
>cite cong.R
>cut C;B;p = C;B;p;C
>pub C;q = C;q;C -> C;q* = C;q*;C
>get L0
>cite L1
>use A1
>focus
>d
>cite commut. l
>u r d d
>cite commut. l
>unf
>use A0
>get L1
>cite antisym
>cite *L
>foc
>d
>use A0 l
>u r
>cite idemp. r
>d
>cite id.R r
>u u>cite distrR r
>d
>cite distrL r
>unf
>cite mono.R
>cite mono.L
>cite trans<
   y=? q*;q + 1
>cite mono+R
>cite mono.R
>foc
>r
>cite id.R r
>unf
>cite mono.L
>cite <intro
>cite <1
>cite =<
>foc
>cite commut+ l
q*

1 + q*;q = q*
--------

>unf

current task:
T17: C;q = C;q;C |- 1 + q*;q = q*

>cite unwindR
task completed

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*

>foc

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*

C;q*;C < C;q*
------

>r

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*

C;q*;C < C;q*
         ----

>cite id.R r

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*;1

C;q*;C < C;q*;1
         ------

>unf

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*;1

>cite mono.L
ambiguous unification
specify desired bindings by number:

0: [ x=C y=q*;C z=q*;1 ]
1: [ x=C;q* y=C z=1 ]
? 1
>cite <intro
>cite <1
