Welcome to Abella 2.0.5-dev.
Abella < Kind name, action, proc type.

Abella < Import "ccs_core".
Importing from "ccs_core".
Warning: Definition can be used to defeat stratification
 (higher-order argument "Tech" occurs to the left of ->)
Warning: Definition can be used to defeat stratification
 (higher-order argument "Rel" occurs to the left of ->)
Warning: Definition can be used to defeat stratification
 (higher-order argument "Rel" occurs to the left of ->)

Abella < Import "ccs_ctx".
Importing from "ccs_ctx".
Warning: Definition can be used to defeat stratification
 (higher-order argument "Rel" occurs to the left of ->)

Abella < Import "ccs_bisim".
Importing from "ccs_bisim".
Warning: Definition can be used to defeat stratification
 (higher-order argument "Tech" occurs to the left of ->)
Warning: Definition can be used to defeat stratification
 (higher-order argument "Tech" occurs to the left of ->)

Abella < Import "ccs_context".
Importing from "ccs_context".

Abella < Define bisim_context_t : proc -> proc -> proc -> proc -> prop by 
bisim_context_t P1 P3 Q1 Q3 := exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ context_t P2 P3 Q2 Q3.

Abella < Theorem bisim_context_t_reflexive : 
forall P, bisim_context_t P P P P.


============================
 forall P, bisim_context_t P P P P

bisim_context_t_reflexive < intros.

Variables: P
============================
 bisim_context_t P P P P

bisim_context_t_reflexive < unfold.

Variables: P
============================
 exists P2 Q2, bisim_t P P2 P Q2 /\ context_t P2 P Q2 P

bisim_context_t_reflexive < witness P.

Variables: P
============================
 exists Q2, bisim_t P P P Q2 /\ context_t P P Q2 P

bisim_context_t_reflexive < witness P.

Variables: P
============================
 bisim_t P P P P /\ context_t P P P P

bisim_context_t_reflexive < split.
Subgoal 1:

Variables: P
============================
 bisim_t P P P P

Subgoal 2 is:
 context_t P P P P

bisim_context_t_reflexive < backchain bisim_t_reflexive.
Subgoal 2:

Variables: P
============================
 context_t P P P P

bisim_context_t_reflexive < search.
Proof completed.
Abella < Theorem bisim_context_reflexive : 
forall P, bisim_up_to bisim_context_t P P.


============================
 forall P, bisim_up_to bisim_context_t P P

bisim_context_reflexive < coinduction.

CH : forall P, bisim_up_to bisim_context_t P P +
============================
 forall P, bisim_up_to bisim_context_t P P #

bisim_context_reflexive < intros.

Variables: P
CH : forall P, bisim_up_to bisim_context_t P P +
============================
 bisim_up_to bisim_context_t P P #

bisim_context_reflexive < unfold.
Subgoal 1:

Variables: P
CH : forall P, bisim_up_to bisim_context_t P P +
============================
 forall A P1, one P A P1 ->
   (exists Q1, one P A Q1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < intros.
Subgoal 1:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 exists Q1, one P A Q1 /\
   (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
        bisim_up_to bisim_context_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < witness P1.
Subgoal 1:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 one P A P1 /\
   (exists P2 Q2, bisim_context_t P1 P2 P1 Q2 /\
        bisim_up_to bisim_context_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < split.
Subgoal 1.1:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 one P A P1

Subgoal 1.2 is:
 exists P2 Q2, bisim_context_t P1 P2 P1 Q2 /\
   bisim_up_to bisim_context_t P2 Q2 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < search.
Subgoal 1.2:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 exists P2 Q2, bisim_context_t P1 P2 P1 Q2 /\
   bisim_up_to bisim_context_t P2 Q2 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < witness P1.
Subgoal 1.2:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 exists Q2, bisim_context_t P1 P1 P1 Q2 /\
   bisim_up_to bisim_context_t P1 Q2 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < witness P1.
Subgoal 1.2:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 bisim_context_t P1 P1 P1 P1 /\ bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < split.
Subgoal 1.2.1:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 bisim_context_t P1 P1 P1 P1

Subgoal 1.2.2 is:
 bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < unfold.
Subgoal 1.2.1:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 exists P2 Q2, bisim_t P1 P2 P1 Q2 /\ context_t P2 P1 Q2 P1

Subgoal 1.2.2 is:
 bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < witness P1.
Subgoal 1.2.1:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 exists Q2, bisim_t P1 P1 P1 Q2 /\ context_t P1 P1 Q2 P1

Subgoal 1.2.2 is:
 bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < witness P1.
Subgoal 1.2.1:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 bisim_t P1 P1 P1 P1 /\ context_t P1 P1 P1 P1

Subgoal 1.2.2 is:
 bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < split.
Subgoal 1.2.1.1:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 bisim_t P1 P1 P1 P1

Subgoal 1.2.1.2 is:
 context_t P1 P1 P1 P1

Subgoal 1.2.2 is:
 bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < unfold.
Subgoal 1.2.1.1.1:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 bisim_up_to refl_t P1 P1

Subgoal 1.2.1.1.2 is:
 bisim_up_to refl_t P1 P1

Subgoal 1.2.1.2 is:
 context_t P1 P1 P1 P1

Subgoal 1.2.2 is:
 bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < backchain bisim_reflexive_.
Subgoal 1.2.1.1.2:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 bisim_up_to refl_t P1 P1

Subgoal 1.2.1.2 is:
 context_t P1 P1 P1 P1

Subgoal 1.2.2 is:
 bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < backchain bisim_reflexive_.
Subgoal 1.2.1.2:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 context_t P1 P1 P1 P1

Subgoal 1.2.2 is:
 bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < search.
Subgoal 1.2.2:

Variables: P A P1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A P1
============================
 bisim_up_to bisim_context_t P1 P1 +

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < backchain CH.
Subgoal 2:

Variables: P
CH : forall P, bisim_up_to bisim_context_t P P +
============================
 forall A Q1, one P A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
             bisim_up_to bisim_context_t P2 Q2 +))

bisim_context_reflexive < intros.
Subgoal 2:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, bisim_context_t P1 P2 Q1 Q2 /\
        bisim_up_to bisim_context_t P2 Q2 +)

bisim_context_reflexive < witness Q1.
Subgoal 2:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 one P A Q1 /\
   (exists P2 Q2, bisim_context_t Q1 P2 Q1 Q2 /\
        bisim_up_to bisim_context_t P2 Q2 +)

bisim_context_reflexive < split.
Subgoal 2.1:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 one P A Q1

Subgoal 2.2 is:
 exists P2 Q2, bisim_context_t Q1 P2 Q1 Q2 /\
   bisim_up_to bisim_context_t P2 Q2 +

bisim_context_reflexive < search.
Subgoal 2.2:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 exists P2 Q2, bisim_context_t Q1 P2 Q1 Q2 /\
   bisim_up_to bisim_context_t P2 Q2 +

bisim_context_reflexive < witness Q1.
Subgoal 2.2:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 exists Q2, bisim_context_t Q1 Q1 Q1 Q2 /\
   bisim_up_to bisim_context_t Q1 Q2 +

bisim_context_reflexive < witness Q1.
Subgoal 2.2:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 bisim_context_t Q1 Q1 Q1 Q1 /\ bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < split.
Subgoal 2.2.1:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 bisim_context_t Q1 Q1 Q1 Q1

Subgoal 2.2.2 is:
 bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < unfold.
Subgoal 2.2.1:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 exists P2 Q2, bisim_t Q1 P2 Q1 Q2 /\ context_t P2 Q1 Q2 Q1

Subgoal 2.2.2 is:
 bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < witness Q1.
Subgoal 2.2.1:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 exists Q2, bisim_t Q1 Q1 Q1 Q2 /\ context_t Q1 Q1 Q2 Q1

Subgoal 2.2.2 is:
 bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < witness Q1.
Subgoal 2.2.1:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 bisim_t Q1 Q1 Q1 Q1 /\ context_t Q1 Q1 Q1 Q1

Subgoal 2.2.2 is:
 bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < split.
Subgoal 2.2.1.1:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 bisim_t Q1 Q1 Q1 Q1

Subgoal 2.2.1.2 is:
 context_t Q1 Q1 Q1 Q1

Subgoal 2.2.2 is:
 bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < unfold.
Subgoal 2.2.1.1.1:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 bisim_up_to refl_t Q1 Q1

Subgoal 2.2.1.1.2 is:
 bisim_up_to refl_t Q1 Q1

Subgoal 2.2.1.2 is:
 context_t Q1 Q1 Q1 Q1

Subgoal 2.2.2 is:
 bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < backchain bisim_reflexive_.
Subgoal 2.2.1.1.2:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 bisim_up_to refl_t Q1 Q1

Subgoal 2.2.1.2 is:
 context_t Q1 Q1 Q1 Q1

Subgoal 2.2.2 is:
 bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < backchain bisim_reflexive_.
Subgoal 2.2.1.2:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 context_t Q1 Q1 Q1 Q1

Subgoal 2.2.2 is:
 bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < search.
Subgoal 2.2.2:

Variables: P A Q1
CH : forall P, bisim_up_to bisim_context_t P P +
H1 : one P A Q1
============================
 bisim_up_to bisim_context_t Q1 Q1 +

bisim_context_reflexive < backchain CH.
Proof completed.
Abella < Theorem bisim_context_t_contexts : 
forall C P1 P2 Q1 Q2, at C P2 P1 -> at C Q2 Q1 -> bisim_context_t P1 P2 Q1 Q2.


============================
 forall C P1 P2 Q1 Q2, at C P2 P1 -> at C Q2 Q1 ->
   bisim_context_t P1 P2 Q1 Q2

bisim_context_t_contexts < intros.

Variables: C P1 P2 Q1 Q2
H1 : at C P2 P1
H2 : at C Q2 Q1
============================
 bisim_context_t P1 P2 Q1 Q2

bisim_context_t_contexts < unfold.

Variables: C P1 P2 Q1 Q2
H1 : at C P2 P1
H2 : at C Q2 Q1
============================
 exists P3 Q3, bisim_t P1 P3 Q1 Q3 /\ context_t P3 P2 Q3 Q2

bisim_context_t_contexts < witness P1.

Variables: C P1 P2 Q1 Q2
H1 : at C P2 P1
H2 : at C Q2 Q1
============================
 exists Q3, bisim_t P1 P1 Q1 Q3 /\ context_t P1 P2 Q3 Q2

bisim_context_t_contexts < witness Q1.

Variables: C P1 P2 Q1 Q2
H1 : at C P2 P1
H2 : at C Q2 Q1
============================
 bisim_t P1 P1 Q1 Q1 /\ context_t P1 P2 Q1 Q2

bisim_context_t_contexts < split.
Subgoal 1:

Variables: C P1 P2 Q1 Q2
H1 : at C P2 P1
H2 : at C Q2 Q1
============================
 bisim_t P1 P1 Q1 Q1

Subgoal 2 is:
 context_t P1 P2 Q1 Q2

bisim_context_t_contexts < unfold.
Subgoal 1.1:

Variables: C P1 P2 Q1 Q2
H1 : at C P2 P1
H2 : at C Q2 Q1
============================
 bisim_up_to refl_t P1 P1

Subgoal 1.2 is:
 bisim_up_to refl_t Q1 Q1

Subgoal 2 is:
 context_t P1 P2 Q1 Q2

bisim_context_t_contexts < backchain bisim_reflexive_.
Subgoal 1.2:

Variables: C P1 P2 Q1 Q2
H1 : at C P2 P1
H2 : at C Q2 Q1
============================
 bisim_up_to refl_t Q1 Q1

Subgoal 2 is:
 context_t P1 P2 Q1 Q2

bisim_context_t_contexts < backchain bisim_reflexive_.
Subgoal 2:

Variables: C P1 P2 Q1 Q2
H1 : at C P2 P1
H2 : at C Q2 Q1
============================
 context_t P1 P2 Q1 Q2

bisim_context_t_contexts < search.
Proof completed.
Abella < Theorem bisim_substitutive_ : 
forall C P1 Q1 P2 Q2, at C P1 Q1 -> at C P2 Q2 -> bisim_up_to refl_t P1 P2 ->
  bisim_up_to refl_t Q1 Q2.


============================
 forall C P1 Q1 P2 Q2, at C P1 Q1 -> at C P2 Q2 ->
   bisim_up_to refl_t P1 P2 -> bisim_up_to refl_t Q1 Q2

bisim_substitutive_ < apply bisim_substitutive.

H1 : substitutive_rel (bisim_up_to refl_t)
============================
 forall C P1 Q1 P2 Q2, at C P1 Q1 -> at C P2 Q2 ->
   bisim_up_to refl_t P1 P2 -> bisim_up_to refl_t Q1 Q2

bisim_substitutive_ < case H1.

H2 : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to refl_t P1 P2 -> bisim_up_to refl_t Q1 Q2
============================
 forall C P1 Q1 P2 Q2, at C P1 Q1 -> at C P2 Q2 ->
   bisim_up_to refl_t P1 P2 -> bisim_up_to refl_t Q1 Q2

bisim_substitutive_ < intros.

Variables: C P1 Q1 P2 Q2
H2 : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to refl_t P1 P2 -> bisim_up_to refl_t Q1 Q2
H3 : at C P1 Q1
H4 : at C P2 Q2
H5 : bisim_up_to refl_t P1 P2
============================
 bisim_up_to refl_t Q1 Q2

bisim_substitutive_ < backchain H2.
Proof completed.
Abella < Theorem ctx_mirror : 
forall C P1 P2 Q1, at C P1 P2 -> (exists Q2, at C Q1 Q2).


============================
 forall C P1 P2 Q1, at C P1 P2 -> (exists Q2, at C Q1 Q2)

ctx_mirror < induction on 1.

IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
============================
 forall C P1 P2 Q1, at C P1 P2 @ -> (exists Q2, at C Q1 Q2)

ctx_mirror < intros.

Variables: C P1 P2 Q1
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H1 : at C P1 P2 @
============================
 exists Q2, at C Q1 Q2

ctx_mirror < case H1.
Subgoal 1:

Variables: P2 Q1
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
============================
 exists Q2, at hole Q1 Q2

Subgoal 2 is:
 exists Q2, at (plus_l C1 R) Q1 Q2

Subgoal 3 is:
 exists Q2, at (plus_r R C1) Q1 Q2

Subgoal 4 is:
 exists Q2, at (par_l C1 R) Q1 Q2

Subgoal 5 is:
 exists Q2, at (par_r R C1) Q1 Q2

Subgoal 6 is:
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < search.
Subgoal 2:

Variables: P1 Q1 R Q C1
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
============================
 exists Q2, at (plus_l C1 R) Q1 Q2

Subgoal 3 is:
 exists Q2, at (plus_r R C1) Q1 Q2

Subgoal 4 is:
 exists Q2, at (par_l C1 R) Q1 Q2

Subgoal 5 is:
 exists Q2, at (par_r R C1) Q1 Q2

Subgoal 6 is:
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < apply IH to H2 with Q1 = Q1.
Subgoal 2:

Variables: P1 Q1 R Q C1 Q2
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
H3 : at C1 Q1 Q2
============================
 exists Q2, at (plus_l C1 R) Q1 Q2

Subgoal 3 is:
 exists Q2, at (plus_r R C1) Q1 Q2

Subgoal 4 is:
 exists Q2, at (par_l C1 R) Q1 Q2

Subgoal 5 is:
 exists Q2, at (par_r R C1) Q1 Q2

Subgoal 6 is:
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < search.
Subgoal 3:

Variables: P1 Q1 Q R C1
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
============================
 exists Q2, at (plus_r R C1) Q1 Q2

Subgoal 4 is:
 exists Q2, at (par_l C1 R) Q1 Q2

Subgoal 5 is:
 exists Q2, at (par_r R C1) Q1 Q2

Subgoal 6 is:
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < apply IH to H2 with Q1 = Q1.
Subgoal 3:

Variables: P1 Q1 Q R C1 Q2
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
H3 : at C1 Q1 Q2
============================
 exists Q2, at (plus_r R C1) Q1 Q2

Subgoal 4 is:
 exists Q2, at (par_l C1 R) Q1 Q2

Subgoal 5 is:
 exists Q2, at (par_r R C1) Q1 Q2

Subgoal 6 is:
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < search.
Subgoal 4:

Variables: P1 Q1 R Q C1
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
============================
 exists Q2, at (par_l C1 R) Q1 Q2

Subgoal 5 is:
 exists Q2, at (par_r R C1) Q1 Q2

Subgoal 6 is:
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < apply IH to H2 with Q1 = Q1.
Subgoal 4:

Variables: P1 Q1 R Q C1 Q2
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
H3 : at C1 Q1 Q2
============================
 exists Q2, at (par_l C1 R) Q1 Q2

Subgoal 5 is:
 exists Q2, at (par_r R C1) Q1 Q2

Subgoal 6 is:
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < search.
Subgoal 5:

Variables: P1 Q1 Q R C1
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
============================
 exists Q2, at (par_r R C1) Q1 Q2

Subgoal 6 is:
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < apply IH to H2 with Q1 = Q1.
Subgoal 5:

Variables: P1 Q1 Q R C1 Q2
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
H3 : at C1 Q1 Q2
============================
 exists Q2, at (par_r R C1) Q1 Q2

Subgoal 6 is:
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < search.
Subgoal 6:

Variables: P1 Q1 Q A C1
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
============================
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < apply IH to H2 with Q1 = Q1.
Subgoal 6:

Variables: P1 Q1 Q A C1 Q2
IH : forall C P1 P2 Q1, at C P1 P2 * -> (exists Q2, at C Q1 Q2)
H2 : at C1 P1 Q *
H3 : at C1 Q1 Q2
============================
 exists Q2, at (act_d A C1) Q1 Q2

ctx_mirror < search.
Proof completed.
Abella < Theorem bisim_context_substitutive : 
substitutive_rel (bisim_up_to bisim_context_t).


============================
 substitutive_rel (bisim_up_to bisim_context_t)

bisim_context_substitutive < unfold.

============================
 forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
   bisim_up_to bisim_context_t P1 P2 -> bisim_up_to bisim_context_t Q1 Q2

bisim_context_substitutive < coinduction.

CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
============================
 forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
   bisim_up_to bisim_context_t P1 P2 -> bisim_up_to bisim_context_t Q1 Q2 #

bisim_context_substitutive < intros.

Variables: P1 P2 C Q1 Q2
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
============================
 bisim_up_to bisim_context_t Q1 Q2 #

bisim_context_substitutive < unfold.
Subgoal 1:

Variables: P1 P2 C Q1 Q2
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
============================
 forall A P1, one Q1 A P1 ->
   (exists Q3, one Q2 A Q3 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < intros.
Subgoal 1:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply ctx_faithful to H1 H4.
Subgoal 1:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H5 : (exists CC, at CC P1 P3 /\
          (forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR))) \/
       (exists CC PBP B, one P1 B PBP /\ at CC PBP P3 /\
            (forall Q QBQ, one Q B QBQ ->
                 (forall Q0, at C Q Q0 ->
                      (exists RR, one Q0 A RR /\ at CC QBQ RR)))) \/
       (forall Q Q0, at C Q Q0 -> one Q0 A P3)
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < case H5.
Subgoal 1.1:

Variables: P1 P2 C Q1 Q2 A P3 CC
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.2 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply H7 to H2.
Subgoal 1.1:

Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.2 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < witness RR.
Subgoal 1.1:

Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
 one Q2 A RR /\
   (exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.2 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < split.
Subgoal 1.1.1:

Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
 one Q2 A RR

Subgoal 1.1.2 is:
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.2 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < search.
Subgoal 1.1.2:

Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.2 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < witness P1.
Subgoal 1.1.2:

Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
 exists Q4, bisim_context_t P3 P1 RR Q4 /\
   bisim_up_to bisim_context_t P1 Q4 +

Subgoal 1.2 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < witness P2.
Subgoal 1.1.2:

Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
 bisim_context_t P3 P1 RR P2 /\ bisim_up_to bisim_context_t P1 P2 +

Subgoal 1.2 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < split.
Subgoal 1.1.2.1:

Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
 bisim_context_t P3 P1 RR P2

Subgoal 1.1.2.2 is:
 bisim_up_to bisim_context_t P1 P2 +

Subgoal 1.2 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < backchain bisim_context_t_contexts.
Subgoal 1.1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
 bisim_up_to bisim_context_t P1 P2 +

Subgoal 1.2 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < backchain CH.
Subgoal 1.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < case H3.
Subgoal 1.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply H9 to H6.
Subgoal 1.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H12 : bisim_context_t PBP P4 Q3 Q4
H13 : bisim_up_to bisim_context_t P4 Q4
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply H8 to H11.
Subgoal 1.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H12 : bisim_context_t PBP P4 Q3 Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply H14 to H2.
Subgoal 1.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H12 : bisim_context_t PBP P4 Q3 Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < witness RR.
Subgoal 1.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H12 : bisim_context_t PBP P4 Q3 Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
============================
 one Q2 A RR /\
   (exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < split.
Subgoal 1.2.1:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H12 : bisim_context_t PBP P4 Q3 Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
============================
 one Q2 A RR

Subgoal 1.2.2 is:
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < search.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H12 : bisim_context_t PBP P4 Q3 Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < case H12.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H17 : bisim_t PBP P5 Q3 Q5
H18 : context_t P5 P4 Q5 Q4
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < case H18.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H17 : bisim_t PBP P5 Q3 Q5
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < case H17.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply ctx_mirror to H7 with Q1 = P5.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1 Q6
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
H23 : at CC P5 Q6
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply ctx_mirror to H16 with Q1 = Q5.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1 Q6 Q7
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply bisim_substitutive_ to H7 H23 H21.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1 Q6 Q7
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t P3 Q6
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply bisim_substitutive_ to H16 H24 H22.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1 Q6 Q7
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t P3 Q6
H26 : bisim_up_to refl_t RR Q7
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply concat_ctx2 to H19 H23 H20 H24.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t P3 Q6
H26 : bisim_up_to refl_t RR Q7
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 exists P2 Q4, bisim_context_t P3 P2 RR Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < witness P4.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t P3 Q6
H26 : bisim_up_to refl_t RR Q7
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 exists Q4, bisim_context_t P3 P4 RR Q4 /\
   bisim_up_to bisim_context_t P4 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < witness Q4.
Subgoal 1.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t P3 Q6
H26 : bisim_up_to refl_t RR Q7
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 bisim_context_t P3 P4 RR Q4 /\ bisim_up_to bisim_context_t P4 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < split.
Subgoal 1.2.2.1:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t P3 Q6
H26 : bisim_up_to refl_t RR Q7
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 bisim_context_t P3 P4 RR Q4

Subgoal 1.2.2.2 is:
 bisim_up_to bisim_context_t P4 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < search.
Subgoal 1.2.2.2:

Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t PBP P5
H22 : bisim_up_to refl_t Q3 Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t P3 Q6
H26 : bisim_up_to refl_t RR Q7
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 bisim_up_to bisim_context_t P4 Q4 +

Subgoal 1.3 is:
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < backchain CH.
Subgoal 1.3:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < apply H6 to H2.
Subgoal 1.3:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
 exists Q3, one Q2 A Q3 /\
   (exists P2 Q4, bisim_context_t P3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < witness P3.
Subgoal 1.3:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
 one Q2 A P3 /\
   (exists P2 Q4, bisim_context_t P3 P2 P3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < split.
Subgoal 1.3.1:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
 one Q2 A P3

Subgoal 1.3.2 is:
 exists P2 Q4, bisim_context_t P3 P2 P3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < search.
Subgoal 1.3.2:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
 exists P2 Q4, bisim_context_t P3 P2 P3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < witness P3.
Subgoal 1.3.2:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
 exists Q4, bisim_context_t P3 P3 P3 Q4 /\
   bisim_up_to bisim_context_t P3 Q4 +

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < witness P3.
Subgoal 1.3.2:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
 bisim_context_t P3 P3 P3 P3 /\ bisim_up_to bisim_context_t P3 P3 +

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < split.
Subgoal 1.3.2.1:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
 bisim_context_t P3 P3 P3 P3

Subgoal 1.3.2.2 is:
 bisim_up_to bisim_context_t P3 P3 +

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < backchain bisim_context_t_reflexive.
Subgoal 1.3.2.2:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
 bisim_up_to bisim_context_t P3 P3 +

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < backchain CH.
Subgoal 1.3.2.2:

Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
 bisim_up_to bisim_context_t P3 P3

Subgoal 2 is:
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < backchain bisim_context_reflexive.
Subgoal 2:

Variables: P1 P2 C Q1 Q2
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
============================
 forall A Q3, one Q2 A Q3 ->
   (exists P1, one Q1 A P1 /\
        (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
             bisim_up_to bisim_context_t P2 Q4 +))

bisim_context_substitutive < intros.
Subgoal 2:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply ctx_faithful to H2 H4.
Subgoal 2:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H5 : (exists CC, at CC P2 Q3 /\
          (forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR))) \/
       (exists CC PBP B, one P2 B PBP /\ at CC PBP Q3 /\
            (forall Q QBQ, one Q B QBQ ->
                 (forall Q0, at C Q Q0 ->
                      (exists RR, one Q0 A RR /\ at CC QBQ RR)))) \/
       (forall Q Q0, at C Q Q0 -> one Q0 A Q3)
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < case H5.
Subgoal 2.1:

Variables: P1 P2 C Q1 Q2 A Q3 CC
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.2 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply H7 to H1.
Subgoal 2.1:

Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.2 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < witness RR.
Subgoal 2.1:

Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
 one Q1 A RR /\
   (exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.2 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < split.
Subgoal 2.1.1:

Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
 one Q1 A RR

Subgoal 2.1.2 is:
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.2 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < search.
Subgoal 2.1.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.2 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < witness P1.
Subgoal 2.1.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
 exists Q4, bisim_context_t RR P1 Q3 Q4 /\
   bisim_up_to bisim_context_t P1 Q4 +

Subgoal 2.2 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < witness P2.
Subgoal 2.1.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
 bisim_context_t RR P1 Q3 P2 /\ bisim_up_to bisim_context_t P1 P2 +

Subgoal 2.2 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < split.
Subgoal 2.1.2.1:

Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
 bisim_context_t RR P1 Q3 P2

Subgoal 2.1.2.2 is:
 bisim_up_to bisim_context_t P1 P2 +

Subgoal 2.2 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < backchain bisim_context_t_contexts.
Subgoal 2.1.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
 bisim_up_to bisim_context_t P1 P2 +

Subgoal 2.2 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < backchain CH.
Subgoal 2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < case H3.
Subgoal 2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply H10 to H6.
Subgoal 2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H12 : bisim_context_t P3 P4 PBP Q4
H13 : bisim_up_to bisim_context_t P4 Q4
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply H8 to H11.
Subgoal 2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H12 : bisim_context_t P3 P4 PBP Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply H14 to H1.
Subgoal 2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H12 : bisim_context_t P3 P4 PBP Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < witness RR.
Subgoal 2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H12 : bisim_context_t P3 P4 PBP Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
============================
 one Q1 A RR /\
   (exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < split.
Subgoal 2.2.1:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H12 : bisim_context_t P3 P4 PBP Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
============================
 one Q1 A RR

Subgoal 2.2.2 is:
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < search.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H12 : bisim_context_t P3 P4 PBP Q4
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < case H12.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H17 : bisim_t P3 P5 PBP Q5
H18 : context_t P5 P4 Q5 Q4
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < case H18.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H17 : bisim_t P3 P5 PBP Q5
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < case H17.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply ctx_mirror to H7 with Q1 = P5.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1 Q6
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
H23 : at CC P5 Q6
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply ctx_mirror to H16 with Q1 = Q5.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1 Q6 Q7
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply bisim_substitutive_ to H7 H24 H22.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1 Q6 Q7
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t Q3 Q7
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply bisim_substitutive_ to H16 H23 H21.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1 Q6 Q7
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t Q3 Q7
H26 : bisim_up_to refl_t RR Q6
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply concat_ctx2 to H19 H23 H20 H24.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t Q3 Q7
H26 : bisim_up_to refl_t RR Q6
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 exists P2 Q4, bisim_context_t RR P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < witness P4.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t Q3 Q7
H26 : bisim_up_to refl_t RR Q6
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 exists Q4, bisim_context_t RR P4 Q3 Q4 /\
   bisim_up_to bisim_context_t P4 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < witness Q4.
Subgoal 2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t Q3 Q7
H26 : bisim_up_to refl_t RR Q6
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 bisim_context_t RR P4 Q3 Q4 /\ bisim_up_to bisim_context_t P4 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < split.
Subgoal 2.2.2.1:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t Q3 Q7
H26 : bisim_up_to refl_t RR Q6
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 bisim_context_t RR P4 Q3 Q4

Subgoal 2.2.2.2 is:
 bisim_up_to bisim_context_t P4 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < search.
Subgoal 2.2.2.2:

Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR P5 Q5 C1 Q6 Q7 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
       (forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
       (exists Q1, one P2 A Q1 /\
            (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                 bisim_up_to bisim_context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
        (exists P3, one P1 A P3 /\
             (exists P4 Q2, bisim_context_t P3 P4 Q1 Q2 /\
                  bisim_up_to bisim_context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to bisim_context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H19 : at C1 P4 P5
H20 : at C1 Q4 Q5
H21 : bisim_up_to refl_t P3 P5
H22 : bisim_up_to refl_t PBP Q5
H23 : at CC P5 Q6
H24 : at CC Q5 Q7
H25 : bisim_up_to refl_t Q3 Q7
H26 : bisim_up_to refl_t RR Q6
H27 : at C3 P4 Q6
H28 : at C3 Q4 Q7
============================
 bisim_up_to bisim_context_t P4 Q4 +

Subgoal 2.3 is:
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < backchain CH.
Subgoal 2.3:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < apply H6 to H1.
Subgoal 2.3:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
 exists P1, one Q1 A P1 /\
   (exists P2 Q4, bisim_context_t P1 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < witness Q3.
Subgoal 2.3:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
 one Q1 A Q3 /\
   (exists P2 Q4, bisim_context_t Q3 P2 Q3 Q4 /\
        bisim_up_to bisim_context_t P2 Q4 +)

bisim_context_substitutive < split.
Subgoal 2.3.1:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
 one Q1 A Q3

Subgoal 2.3.2 is:
 exists P2 Q4, bisim_context_t Q3 P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

bisim_context_substitutive < search.
Subgoal 2.3.2:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
 exists P2 Q4, bisim_context_t Q3 P2 Q3 Q4 /\
   bisim_up_to bisim_context_t P2 Q4 +

bisim_context_substitutive < witness Q3.
Subgoal 2.3.2:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
 exists Q4, bisim_context_t Q3 Q3 Q3 Q4 /\
   bisim_up_to bisim_context_t Q3 Q4 +

bisim_context_substitutive < witness Q3.
Subgoal 2.3.2:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
 bisim_context_t Q3 Q3 Q3 Q3 /\ bisim_up_to bisim_context_t Q3 Q3 +

bisim_context_substitutive < split.
Subgoal 2.3.2.1:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
 bisim_context_t Q3 Q3 Q3 Q3

Subgoal 2.3.2.2 is:
 bisim_up_to bisim_context_t Q3 Q3 +

bisim_context_substitutive < backchain bisim_context_t_reflexive.
Subgoal 2.3.2.2:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
 bisim_up_to bisim_context_t Q3 Q3 +

bisim_context_substitutive < backchain CH.
Subgoal 2.3.2.2:

Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
       bisim_up_to bisim_context_t P1 P2 ->
       bisim_up_to bisim_context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to bisim_context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
 bisim_up_to bisim_context_t Q3 Q3

bisim_context_substitutive < backchain bisim_context_reflexive.
Proof completed.
Abella < Theorem bisim_context_sound_fst : 
is_sound_fst bisim_context_t.


============================
 is_sound_fst bisim_context_t

bisim_context_sound_fst < unfold.

============================
 forall P Q, (exists R S, bisim_up_to refl_t P R /\
                  bisim_up_to bisim_context_t R S /\ bisim_up_to refl_t S Q) ->
   bisim_up_to refl_t P Q

bisim_context_sound_fst < coinduction.

CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
============================
 forall P Q, (exists R S, bisim_up_to refl_t P R /\
                  bisim_up_to bisim_context_t R S /\ bisim_up_to refl_t S Q) ->
   bisim_up_to refl_t P Q #

bisim_context_sound_fst < intros.

Variables: P Q
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H1 : exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_context_t R S /\
       bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q #

bisim_context_sound_fst < case H1.

Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q #

bisim_context_sound_fst < unfold.
Subgoal 1:

Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
============================
 forall A P1, one P A P1 ->
   (exists Q1, one Q A Q1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < intros.
Subgoal 1:

Variables: P Q R S A P1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
H5 : one P A P1
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < case H2.
Subgoal 1:

Variables: P Q R S A P1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
H5 : one P A P1
H6 : forall A P1, one P A P1 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : forall A Q2, one R A Q2 ->
       (exists P1, one P A P1 /\
            (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < clear H7.
Subgoal 1:

Variables: P Q R S A P1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
H5 : one P A P1
H6 : forall A P1, one P A P1 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < apply H6 to H5.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
H5 : one P A P1
H6 : forall A P1, one P A P1 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H8 : one R A Q2
H9 : refl_t P1 P3 Q2 Q3
H10 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < clear H6.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
H5 : one P A P1
H8 : one R A Q2
H9 : refl_t P1 P3 Q2 Q3
H10 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < case H9.
Subgoal 1:

Variables: P Q R S A P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < case H3.
Subgoal 1:

Variables: P Q R S A P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H4 : bisim_up_to refl_t S Q
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : forall A P1, one R A P1 ->
        (exists Q2, one S A Q2 /\
             (exists P3 Q3, bisim_context_t P1 P3 Q2 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
H12 : forall A Q2, one S A Q2 ->
        (exists P1, one R A P1 /\
             (exists P3 Q3, bisim_context_t P1 P3 Q2 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < clear H12.
Subgoal 1:

Variables: P Q R S A P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H4 : bisim_up_to refl_t S Q
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : forall A P1, one R A P1 ->
        (exists Q2, one S A Q2 /\
             (exists P3 Q3, bisim_context_t P1 P3 Q2 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < apply H11 to H8.
Subgoal 1:

Variables: P Q R S A P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H4 : bisim_up_to refl_t S Q
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : forall A P1, one R A P1 ->
        (exists Q2, one S A Q2 /\
             (exists P3 Q3, bisim_context_t P1 P3 Q2 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
H13 : one S A Q1
H14 : bisim_context_t Q3 P2 Q1 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < clear H11.
Subgoal 1:

Variables: P Q R S A P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H4 : bisim_up_to refl_t S Q
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A Q1
H14 : bisim_context_t Q3 P2 Q1 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < case H4.
Subgoal 1:

Variables: P Q R S A P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A Q1
H14 : bisim_context_t Q3 P2 Q1 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H16 : forall A P1, one S A P1 ->
        (exists Q1, one Q A Q1 /\
             (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
H17 : forall A Q1, one Q A Q1 ->
        (exists P1, one S A P1 /\
             (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < clear H17.
Subgoal 1:

Variables: P Q R S A P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A Q1
H14 : bisim_context_t Q3 P2 Q1 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H16 : forall A P1, one S A P1 ->
        (exists Q1, one Q A Q1 /\
             (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < apply H16 to H13.
Subgoal 1:

Variables: P Q R S A P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A Q1
H14 : bisim_context_t Q3 P2 Q1 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H16 : forall A P1, one S A P1 ->
        (exists Q1, one Q A Q1 /\
             (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
H18 : one Q A Q5
H19 : refl_t Q1 P4 Q5 Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < clear H16.
Subgoal 1:

Variables: P Q R S A P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A Q1
H14 : bisim_context_t Q3 P2 Q1 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q5
H19 : refl_t Q1 P4 Q5 Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < case H19.
Subgoal 1:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H14 : bisim_context_t Q3 P2 P4 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 exists Q1, one Q A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < witness Q6.
Subgoal 1:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H14 : bisim_context_t Q3 P2 P4 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 one Q A Q6 /\
   (exists P2 Q2, refl_t P3 P2 Q6 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < split.
Subgoal 1.1:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H14 : bisim_context_t Q3 P2 P4 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 one Q A Q6

Subgoal 1.2 is:
 exists P2 Q2, refl_t P3 P2 Q6 Q2 /\ bisim_up_to refl_t P2 Q2 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < search.
Subgoal 1.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H14 : bisim_context_t Q3 P2 P4 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 exists P2 Q2, refl_t P3 P2 Q6 Q2 /\ bisim_up_to refl_t P2 Q2 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < witness P3.
Subgoal 1.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H14 : bisim_context_t Q3 P2 P4 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 exists Q2, refl_t P3 P3 Q6 Q2 /\ bisim_up_to refl_t P3 Q2 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < witness Q6.
Subgoal 1.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H14 : bisim_context_t Q3 P2 P4 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 refl_t P3 P3 Q6 Q6 /\ bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < split.
Subgoal 1.2.1:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H14 : bisim_context_t Q3 P2 P4 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 refl_t P3 P3 Q6 Q6

Subgoal 1.2.2 is:
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < search.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H14 : bisim_context_t Q3 P2 P4 Q4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < case H14.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H21 : bisim_t Q3 P5 P4 Q7
H22 : context_t P5 P2 Q7 Q4
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < case H21.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < assert bisim_up_to refl_t P3 P5.
Subgoal 1.2.2.1:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
============================
 bisim_up_to refl_t P3 P5

Subgoal 1.2.2 is:
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < backchain bisim_transitive_.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
H25 : bisim_up_to refl_t P3 P5
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < assert bisim_up_to bisim_context_t P5 Q7.
Subgoal 1.2.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
H25 : bisim_up_to refl_t P3 P5
============================
 bisim_up_to bisim_context_t P5 Q7

Subgoal 1.2.2 is:
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < Lem : apply bisim_context_substitutive.
Subgoal 1.2.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
H25 : bisim_up_to refl_t P3 P5
Lem : substitutive_rel (bisim_up_to bisim_context_t)
============================
 bisim_up_to bisim_context_t P5 Q7

Subgoal 1.2.2 is:
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < Lem : case Lem.
Subgoal 1.2.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
H25 : bisim_up_to refl_t P3 P5
Lem : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
        bisim_up_to bisim_context_t P1 P2 ->
        bisim_up_to bisim_context_t Q1 Q2
============================
 bisim_up_to bisim_context_t P5 Q7

Subgoal 1.2.2 is:
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < case H22.
Subgoal 1.2.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7 C
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
H25 : bisim_up_to refl_t P3 P5
Lem : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
        bisim_up_to bisim_context_t P1 P2 ->
        bisim_up_to bisim_context_t Q1 Q2
H26 : at C P2 P5
H27 : at C Q4 Q7
============================
 bisim_up_to bisim_context_t P5 Q7

Subgoal 1.2.2 is:
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < backchain Lem.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
H25 : bisim_up_to refl_t P3 P5
H26 : bisim_up_to bisim_context_t P5 Q7
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < assert bisim_up_to refl_t Q7 Q6.
Subgoal 1.2.2.3:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
H25 : bisim_up_to refl_t P3 P5
H26 : bisim_up_to bisim_context_t P5 Q7
============================
 bisim_up_to refl_t Q7 Q6

Subgoal 1.2.2 is:
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < apply bisim_symmetric_ to H24.
Subgoal 1.2.2.3:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
H25 : bisim_up_to refl_t P3 P5
H26 : bisim_up_to bisim_context_t P5 Q7
H27 : bisim_up_to refl_t Q7 P4
============================
 bisim_up_to refl_t Q7 Q6

Subgoal 1.2.2 is:
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < backchain bisim_transitive_.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6 P5 Q7
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one P A P3
H8 : one R A Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one S A P4
H15 : bisim_up_to bisim_context_t P2 Q4
H18 : one Q A Q6
H20 : bisim_up_to refl_t P4 Q6
H22 : context_t P5 P2 Q7 Q4
H23 : bisim_up_to refl_t Q3 P5
H24 : bisim_up_to refl_t P4 Q7
H25 : bisim_up_to refl_t P3 P5
H26 : bisim_up_to bisim_context_t P5 Q7
H27 : bisim_up_to refl_t Q7 Q6
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < backchain CH.
Subgoal 2:

Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
============================
 forall A Q1, one Q A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_context_sound_fst < intros.
Subgoal 2:

Variables: P Q R S A Q1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
H5 : one Q A Q1
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < case H4.
Subgoal 2:

Variables: P Q R S A Q1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_context_t R S
H5 : one Q A Q1
H6 : forall A P2, one S A P2 ->
       (exists Q1, one Q A Q1 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : forall A Q1, one Q A Q1 ->
       (exists P2, one S A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < apply H7 to H5.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_context_t R S
H5 : one Q A Q1
H6 : forall A P2, one S A P2 ->
       (exists Q1, one Q A Q1 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : forall A Q1, one Q A Q1 ->
       (exists P2, one S A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H8 : one S A P2
H9 : refl_t P2 P3 Q1 Q3
H10 : bisim_up_to refl_t P3 Q3
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < case H3.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H5 : one Q A Q1
H6 : forall A P2, one S A P2 ->
       (exists Q1, one Q A Q1 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : forall A Q1, one Q A Q1 ->
       (exists P2, one S A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H8 : one S A P2
H9 : refl_t P2 P3 Q1 Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : forall A P2, one R A P2 ->
        (exists Q1, one S A Q1 /\
             (exists P3 Q3, bisim_context_t P2 P3 Q1 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
H12 : forall A Q1, one S A Q1 ->
        (exists P2, one R A P2 /\
             (exists P3 Q3, bisim_context_t P2 P3 Q1 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < apply H12 to H8.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H5 : one Q A Q1
H6 : forall A P2, one S A P2 ->
       (exists Q1, one Q A Q1 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : forall A Q1, one Q A Q1 ->
       (exists P2, one S A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H8 : one S A P2
H9 : refl_t P2 P3 Q1 Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : forall A P2, one R A P2 ->
        (exists Q1, one S A Q1 /\
             (exists P3 Q3, bisim_context_t P2 P3 Q1 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
H12 : forall A Q1, one S A Q1 ->
        (exists P2, one R A P2 /\
             (exists P3 Q3, bisim_context_t P2 P3 Q1 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
H13 : one R A P1
H14 : bisim_context_t P1 P4 P2 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < case H2.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q1
H6 : forall A P2, one S A P2 ->
       (exists Q1, one Q A Q1 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : forall A Q1, one Q A Q1 ->
       (exists P2, one S A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H8 : one S A P2
H9 : refl_t P2 P3 Q1 Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : forall A P2, one R A P2 ->
        (exists Q1, one S A Q1 /\
             (exists P3 Q3, bisim_context_t P2 P3 Q1 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
H12 : forall A Q1, one S A Q1 ->
        (exists P2, one R A P2 /\
             (exists P3 Q3, bisim_context_t P2 P3 Q1 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
H13 : one R A P1
H14 : bisim_context_t P1 P4 P2 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H16 : forall A P1, one P A P1 ->
        (exists Q1, one R A Q1 /\
             (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
H17 : forall A Q1, one R A Q1 ->
        (exists P1, one P A P1 /\
             (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < apply H17 to H13.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q1
H6 : forall A P2, one S A P2 ->
       (exists Q1, one Q A Q1 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : forall A Q1, one Q A Q1 ->
       (exists P2, one S A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
H8 : one S A P2
H9 : refl_t P2 P3 Q1 Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : forall A P2, one R A P2 ->
        (exists Q1, one S A Q1 /\
             (exists P3 Q3, bisim_context_t P2 P3 Q1 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
H12 : forall A Q1, one S A Q1 ->
        (exists P2, one R A P2 /\
             (exists P3 Q3, bisim_context_t P2 P3 Q1 Q3 /\
                  bisim_up_to bisim_context_t P3 Q3))
H13 : one R A P1
H14 : bisim_context_t P1 P4 P2 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H16 : forall A P1, one P A P1 ->
        (exists Q1, one R A Q1 /\
             (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
H17 : forall A Q1, one R A Q1 ->
        (exists P1, one P A P1 /\
             (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
H18 : one P A P5
H19 : refl_t P5 P6 P1 Q4
H20 : bisim_up_to refl_t P6 Q4
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < clear H6 H7 H11 H12 H16 H17.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q1
H8 : one S A P2
H9 : refl_t P2 P3 Q1 Q3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A P1
H14 : bisim_context_t P1 P4 P2 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P5
H19 : refl_t P5 P6 P1 Q4
H20 : bisim_up_to refl_t P6 Q4
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < case H9.
Subgoal 2:

Variables: P Q R S A P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A P1
H14 : bisim_context_t P1 P4 P3 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P5
H19 : refl_t P5 P6 P1 Q4
H20 : bisim_up_to refl_t P6 Q4
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < case H19.
Subgoal 2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H14 : bisim_context_t Q4 P4 P3 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < witness P6.
Subgoal 2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H14 : bisim_context_t Q4 P4 P3 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
============================
 one P A P6 /\
   (exists P2 Q2, refl_t P6 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_context_sound_fst < split.
Subgoal 2.1:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H14 : bisim_context_t Q4 P4 P3 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
============================
 one P A P6

Subgoal 2.2 is:
 exists P2 Q2, refl_t P6 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_context_sound_fst < search.
Subgoal 2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H14 : bisim_context_t Q4 P4 P3 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
============================
 exists P2 Q2, refl_t P6 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_context_sound_fst < witness P6.
Subgoal 2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H14 : bisim_context_t Q4 P4 P3 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
============================
 exists Q2, refl_t P6 P6 Q3 Q2 /\ bisim_up_to refl_t P6 Q2 +

bisim_context_sound_fst < witness Q3.
Subgoal 2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H14 : bisim_context_t Q4 P4 P3 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
============================
 refl_t P6 P6 Q3 Q3 /\ bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < split.
Subgoal 2.2.1:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H14 : bisim_context_t Q4 P4 P3 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
============================
 refl_t P6 P6 Q3 Q3

Subgoal 2.2.2 is:
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < search.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H14 : bisim_context_t Q4 P4 P3 Q2
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
============================
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < case H14.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H21 : bisim_t Q4 P7 P3 Q5
H22 : context_t P7 P4 Q5 Q2
============================
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < case H21.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
============================
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < assert bisim_up_to refl_t P6 P7.
Subgoal 2.2.2.1:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
============================
 bisim_up_to refl_t P6 P7

Subgoal 2.2.2 is:
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < backchain bisim_transitive_.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
H25 : bisim_up_to refl_t P6 P7
============================
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < assert bisim_up_to bisim_context_t P7 Q5.
Subgoal 2.2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
H25 : bisim_up_to refl_t P6 P7
============================
 bisim_up_to bisim_context_t P7 Q5

Subgoal 2.2.2 is:
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < Lem : apply bisim_context_substitutive.
Subgoal 2.2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
H25 : bisim_up_to refl_t P6 P7
Lem : substitutive_rel (bisim_up_to bisim_context_t)
============================
 bisim_up_to bisim_context_t P7 Q5

Subgoal 2.2.2 is:
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < Lem : case Lem.
Subgoal 2.2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
H25 : bisim_up_to refl_t P6 P7
Lem : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
        bisim_up_to bisim_context_t P1 P2 ->
        bisim_up_to bisim_context_t Q1 Q2
============================
 bisim_up_to bisim_context_t P7 Q5

Subgoal 2.2.2 is:
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < case H22.
Subgoal 2.2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5 C
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
H25 : bisim_up_to refl_t P6 P7
Lem : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
        bisim_up_to bisim_context_t P1 P2 ->
        bisim_up_to bisim_context_t Q1 Q2
H26 : at C P4 P7
H27 : at C Q2 Q5
============================
 bisim_up_to bisim_context_t P7 Q5

Subgoal 2.2.2 is:
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < backchain Lem.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
H25 : bisim_up_to refl_t P6 P7
H26 : bisim_up_to bisim_context_t P7 Q5
============================
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < assert bisim_up_to refl_t Q5 Q3.
Subgoal 2.2.2.3:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
H25 : bisim_up_to refl_t P6 P7
H26 : bisim_up_to bisim_context_t P7 Q5
============================
 bisim_up_to refl_t Q5 Q3

Subgoal 2.2.2 is:
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < apply bisim_symmetric_ to H24.
Subgoal 2.2.2.3:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
H25 : bisim_up_to refl_t P6 P7
H26 : bisim_up_to bisim_context_t P7 Q5
H27 : bisim_up_to refl_t Q5 P3
============================
 bisim_up_to refl_t Q5 Q3

Subgoal 2.2.2 is:
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < backchain bisim_transitive_.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4 P7 Q5
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_context_t R S /\
                      bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H5 : one Q A Q3
H8 : one S A P3
H10 : bisim_up_to refl_t P3 Q3
H13 : one R A Q4
H15 : bisim_up_to bisim_context_t P4 Q2
H18 : one P A P6
H20 : bisim_up_to refl_t P6 Q4
H22 : context_t P7 P4 Q5 Q2
H23 : bisim_up_to refl_t Q4 P7
H24 : bisim_up_to refl_t P3 Q5
H25 : bisim_up_to refl_t P6 P7
H26 : bisim_up_to bisim_context_t P7 Q5
H27 : bisim_up_to refl_t Q5 Q3
============================
 bisim_up_to refl_t P6 Q3 +

bisim_context_sound_fst < backchain CH.
Proof completed.
Abella < Theorem bisim_context_sound_snd : 
is_sound_snd bisim_context_t.


============================
 is_sound_snd bisim_context_t

bisim_context_sound_snd < unfold.

============================
 forall P Q, bisim_up_to bisim_context_t P Q ->
   (exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_context_t R S /\
        bisim_up_to refl_t S Q)

bisim_context_sound_snd < intros.

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
============================
 exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_context_t R S /\
   bisim_up_to refl_t S Q

bisim_context_sound_snd < witness P.

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
============================
 exists S, bisim_up_to refl_t P P /\ bisim_up_to bisim_context_t P S /\
   bisim_up_to refl_t S Q

bisim_context_sound_snd < witness Q.

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
============================
 bisim_up_to refl_t P P /\ bisim_up_to bisim_context_t P Q /\
   bisim_up_to refl_t Q Q

bisim_context_sound_snd < split.
Subgoal 1:

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
============================
 bisim_up_to refl_t P P

Subgoal 2 is:
 bisim_up_to bisim_context_t P Q

Subgoal 3 is:
 bisim_up_to refl_t Q Q

bisim_context_sound_snd < backchain bisim_reflexive_.
Subgoal 2:

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
============================
 bisim_up_to bisim_context_t P Q

Subgoal 3 is:
 bisim_up_to refl_t Q Q

bisim_context_sound_snd < search.
Subgoal 3:

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
============================
 bisim_up_to refl_t Q Q

bisim_context_sound_snd < backchain bisim_reflexive_.
Proof completed.
Abella < Theorem bisim_context_sound : 
is_sound bisim_context_t.


============================
 is_sound bisim_context_t

bisim_context_sound < unfold.

============================
 forall P Q, bisim_up_to bisim_context_t P Q -> bisim_up_to refl_t P Q

bisim_context_sound < intros.

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
============================
 bisim_up_to refl_t P Q

bisim_context_sound < Snd : apply bisim_context_sound_snd.

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
Snd : is_sound_snd bisim_context_t
============================
 bisim_up_to refl_t P Q

bisim_context_sound < Snd : case Snd.

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
Snd : forall P Q, bisim_up_to bisim_context_t P Q ->
        (exists R S, bisim_up_to refl_t P R /\
             bisim_up_to bisim_context_t R S /\ bisim_up_to refl_t S Q)
============================
 bisim_up_to refl_t P Q

bisim_context_sound < Fst : apply bisim_context_sound_fst.

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
Snd : forall P Q, bisim_up_to bisim_context_t P Q ->
        (exists R S, bisim_up_to refl_t P R /\
             bisim_up_to bisim_context_t R S /\ bisim_up_to refl_t S Q)
Fst : is_sound_fst bisim_context_t
============================
 bisim_up_to refl_t P Q

bisim_context_sound < Fst : case Fst.

Variables: P Q
H1 : bisim_up_to bisim_context_t P Q
Snd : forall P Q, bisim_up_to bisim_context_t P Q ->
        (exists R S, bisim_up_to refl_t P R /\
             bisim_up_to bisim_context_t R S /\ bisim_up_to refl_t S Q)
Fst : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                       bisim_up_to bisim_context_t R S /\
                       bisim_up_to refl_t S Q) ->
        bisim_up_to refl_t P Q
============================
 bisim_up_to refl_t P Q

bisim_context_sound < apply Snd to H1.

Variables: P Q R S
H1 : bisim_up_to bisim_context_t P Q
Snd : forall P Q, bisim_up_to bisim_context_t P Q ->
        (exists R S, bisim_up_to refl_t P R /\
             bisim_up_to bisim_context_t R S /\ bisim_up_to refl_t S Q)
Fst : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                       bisim_up_to bisim_context_t R S /\
                       bisim_up_to refl_t S Q) ->
        bisim_up_to refl_t P Q
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_context_t R S
H4 : bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q

bisim_context_sound < backchain Fst.
Proof completed.
Abella <