Require Export Bisimulation.

Inductive struct_congr {V : Set} : binary (proc V) :=
| sc_par_assoc : ∀ P Q R, struct_congr (P // (Q // R)) ((P // Q) // R)
| sc_par_assoc_rev : ∀ P Q R, struct_congr ((P // Q) // R) (P // (Q // R))
| sc_par_comm : ∀ P Q, struct_congr (P // Q) (Q // P)
| sc_par_nil : ∀ P, struct_congr (P // PO) P
| sc_par_nil_conv : ∀ P, struct_congr P (P // PO)
| sc_scope: ∀ P Q, (∀ a, notin_ho a Q → notin a (Q a)) →
      ∀ a, struct_congr (nu (fun x ⇒ (P x // Q x))) ((nu P) // Q a)
| sc_scope_rev: ∀ P Q, (∀ a, notin_ho a Q → notin a (Q a)) →
      ∀ a, struct_congr ((nu P) // Q a) (nu (fun x ⇒ (P x // Q x)))
| sc_nu_nil : struct_congr (nu (fun x ⇒ PO)) PO
| sc_nu_nil_rev : struct_congr PO (nu (fun x ⇒ PO))
| sc_nu_nu : ∀ P, struct_congr (nu (fun x ⇒ nu (fun y ⇒ P x y))) (nu (fun y ⇒ nu (fun x ⇒ P x y)))
| sc_nil : struct_congr PO PO
| sc_var : ∀ x, struct_congr (pr_var x) (pr_var x)
| sc_par : ∀ P Q P' Q', struct_congr P Q → struct_congr P' Q'
                                              → struct_congr (P // P') (Q // Q')
| sc_inp : ∀ a P Q, @struct_congr (incV V) P Q → struct_congr (a? P) (a? Q)
| sc_out : ∀ a P Q P' Q', struct_congr P Q → struct_congr P' Q'
                                                 → struct_congr (a!(P) P') (a!(Q) Q')
| sc_nu : ∀ P Q L, (∀ a, ¬In a L →
                      struct_congr (P a)(Q a)) → struct_congr (nu P) (nu Q)
| sc_trans : ∀ P Q R, struct_congr P Q → struct_congr Q R → struct_congr P R
.

Lemma struct_congr_ind'
     : ∀ Pr : ∀ V : Set, proc V → proc V → Prop,
       (∀ (V : Set) (P Q R : proc V),
        Pr V (P // (Q // R)) (P // Q // R)) →
       (∀ (V : Set) (P Q R : proc V),
        Pr V (P // Q // R) (P // (Q // R))) →
       (∀ (V : Set) (P Q : proc V), Pr V (P // Q) (Q // P)) →
       (∀ (V : Set) (P : proc V), Pr V (P // PO) P) →
       (∀ (V : Set) (P : proc V), Pr V P (P // PO)) →
       (∀ (V : Set) (P Q : name → proc V),
        (∀ a : name, notin_ho a Q → notin a (Q a)) →
        ∀ a : name,
        Pr V (nu (fun x : name ⇒ P x // Q x)) ((nu P) // Q a)) →
       (∀ (V : Set) (P Q : name → proc V),
        (∀ a : name, notin_ho a Q → notin a (Q a)) →
        ∀ a : name, notin_ho a Q →
        Pr V ((nu P) // Q a) (nu (fun x : name ⇒ P x // Q x))) →
       (∀ V : Set, Pr V (nu (fun _ : name ⇒ PO)) PO) →
       (∀ V : Set, Pr V PO (nu (fun _ : name ⇒ PO))) →
       (∀ (V : Set) (P : name → name → proc V),
        Pr V (nu (fun x : name ⇒ nu (fun y : name ⇒ P x y)))
          (nu (fun y : name ⇒ nu (fun x : name ⇒ P x y)))) →
       (∀ V : Set, Pr V PO PO) →
       (∀ (V : Set) (x : V), Pr V (pr_var x) (pr_var x)) →
       (∀ (V : Set) (P Q P' Q' : proc V),
        struct_congr P Q →
        Pr V P Q →
        struct_congr P' Q' → Pr V P' Q' → Pr V (P // P') (Q // Q')) →
       (∀ (V : Set) (a : name) (P Q : proc (incV V)),
        struct_congr P Q → Pr (incV V) P Q → Pr V (a ? P) (a ? Q)) →
       (∀ (V : Set) (a : name) (P Q P' Q' : proc V),
        struct_congr P Q →
        Pr V P Q →
        struct_congr P' Q' → Pr V P' Q' → Pr V (a !( P) P') (a !( Q) Q')) →
       (∀ (V : Set) (P Q : name → proc V) (L : list name),
        (∀ a : name, ¬ In a L → struct_congr (P a) (Q a)) →
        (∀ a : name, ¬ In a L → Pr V (P a) (Q a)) → Pr V (nu P) (nu Q)) →
       (∀ (V : Set) (P Q R : proc V),
        struct_congr P Q →
        Pr V P Q → struct_congr Q R → Pr V Q R → Pr V P R) →
       ∀ (V : Set) (p p0 : proc V), struct_congr p p0 → Pr V p p0.
Proof.
  intros. induction H16; eauto.
  fresh_proc (nu Q). asserts_rewrite (Q a = Q x).
  apply× @unused_arg. auto.
Qed.

Hint Constructors struct_congr:sc.

Lemma sc_refl {V : Set} : ∀ P, @struct_congr V P P.
Proof.
  induction P; auto with sc.
  forwards*: @sc_nu (@nil name).
Qed.

Lemma sc_symmetric {V : Set} : ∀ (P Q:proc V),
  struct_congr P Q → struct_congr Q P.
Proof.
  intros P Q H. induction H; eauto with sc.
Qed.

Hint Resolve sc_refl sc_symmetric.

Hint Constructors notin:hopi.

Lemma sc_mapV: ∀ (V W:Set) P Q (f:V → W), @struct_congr V P Q
   → @struct_congr W (mapV f P) (mapV f Q).
Proof.
  intros. gen W.
  induction H;
  simpl; auto with sc; try (intros; auto with sc).
  - change (struct_congr (nu (fun x : name ⇒ ((fun x : name ⇒ mapV f (P x)) x) // ((fun x : name ⇒ mapV f (Q x)) x)))
        ((nu (fun x : name ⇒ mapV f (P x))) // ((fun x : name ⇒ mapV f (Q x)) a))).
    apply sc_scope; auto with hopi.
  - change (struct_congr ((nu (fun x : name ⇒ mapV f (P x))) // ((fun x : name ⇒ mapV f (Q x)) a))
        (nu (fun x : name ⇒ ((fun x : name ⇒ mapV f (P x)) x) // ((fun x : name ⇒ mapV f (Q x)) x)))).
    apply sc_scope_rev; auto with hopi.
  - apply sc_nu with L. auto with sc.
  - eapply sc_trans; eauto.
Qed.

Lemma sc_liftV: ∀ (V W:Set) (f:V → proc W) (g:V → proc W),
   (∀ x, @struct_congr W (f x) (g x)) →
   (∀ x, @struct_congr (incV W) (liftV f x) (liftV g x)).
Proof.
  intros.
  destruct x; simpl; auto with sc.
  apply sc_mapV. auto with sc.
Qed.

Lemma sc_bind': ∀ (V W:Set) (P : proc V) (f:V → proc W) (g:V → proc W),
   (∀ x, @struct_congr W (f x) (g x)) →
   @struct_congr W (bind f P) (bind g P).
Proof.
  intros. gen W.
  induction P; intros; simpl; auto with sc.
  - apply sc_inp. apply IHP. intros. apply× sc_liftV.
  - apply sc_nu with (@nil name). auto with sc.
Qed.

Hint Resolve sc_bind' sc_liftV sc_mapV:sc.

Lemma sc_bind: ∀ (V W:Set) (P Q : proc V) (f:V → proc W) (g:V → proc W), @struct_congr V P Q →
   (∀ x, @struct_congr W (f x) (g x)) →
   @struct_congr W (bind f P) (bind g Q).
Proof.
  intros. gen W. induction H; simpl; try solve [auto with sc]; intros.
  - apply sc_trans with (bind f P // (bind f Q // bind g R)); auto with sc.
    apply sc_trans with (bind f P // (bind g Q // bind g R)); eauto with sc.
  - apply sc_trans with (bind f P // bind f Q // bind g R); auto with sc.
    apply sc_trans with (bind f P // bind g Q // bind g R); eauto with sc.
  - eauto with sc.
  - eauto with sc.
  - eauto with sc.
  - apply sc_trans with ((nu (fun x : name ⇒ bind f (P x))) // bind f (Q a)).
    + change (struct_congr (nu (fun x : name ⇒ ((fun x : name ⇒ bind f (P x)) x) // ((fun x : name ⇒ bind f (Q x)) x)))
           ((nu (fun x : name ⇒ bind f (P x))) // ((fun x : name ⇒ bind f (Q x)) a))).
      apply sc_scope; auto with hopi. intros. apply notin_bind; auto with hopi.
      intros. destruct (unsat (a0 ? (@pr_nil (incV V)))).
      simpl_notin. forwards*:H1 x.
      apply notin_bind_rev in H3. intuition.
      apply H4. apply isinV_rename with a0; auto.
    + change (struct_congr (bind f ((nu (fun x : name ⇒ P x)) // Q a))
             (bind g ((nu (fun x : name ⇒ P x)) // Q a))).
      auto with sc.
  - apply sc_trans with ((nu (fun x : name ⇒ bind g (P x))) // bind g (Q a)).
    + change (struct_congr (bind f ((nu (fun x : name ⇒ P x)) // Q a))
             (bind g ((nu (fun x : name ⇒ P x)) // Q a))).
      auto with sc.
    + change (struct_congr ((nu (fun x ⇒ bind g (P x))) // (fun x ⇒ bind g (Q x)) a)
          (nu (fun x : name ⇒ (fun x⇒ bind g (P x)) x // (fun x ⇒ bind g (Q x)) x))).
      apply sc_scope_rev; auto with sc. intros. apply notin_bind; auto with hopi.
      intros. destruct (unsat (a0 ? (@pr_nil (incV V)))). simpl_notin.
      forwards*:H1 x. apply notin_bind_rev in H3.
      intuition. apply H4. apply isinV_rename with a0; auto.
  - apply sc_trans with (nu (fun x : name ⇒ nu (fun x0 : name ⇒ bind g (P x x0))));
      auto with sc.
    change (struct_congr (bind f (nu (fun x : name ⇒ nu (fun x0 : name ⇒ P x x0))))
                         (bind g (nu (fun x : name ⇒ nu (fun x0 : name ⇒ P x x0))))).
    auto with sc.
  - eauto with sc.
  - eauto with sc.
Qed.

Hint Resolve sc_bind:sc.

Lemma sc_appr_appl: ∀ F C,
   struct_congr (appr F C) (appl C F).
Proof.
  intros; induction C; simpl; auto with sc.
  apply sc_nu with (@nil name). auto with sc.
Qed.

Lemma sc_appl_appr: ∀ F C,
   struct_congr (appl C F) (appr F C).
Proof.
  intros; induction C; simpl; auto with sc.
  apply sc_nu with (@nil name). auto with sc.
Qed.

Hint Resolve sc_appl_appr sc_appr_appl:sc.

Lemma sc_rename {V:Set} : ∀ (P Q:name → proc V) a,
  notin_ho a P → notin_ho a Q → struct_congr (P a)(Q a) →
  ∀ b, struct_congr (P b)(Q b).
Proof.
  introv HaP HaQ Hsc.
  remember (P a) as Pa. remember (Q a) as Qa.
  gen a P Q. induction Hsc; intros;
    try solve [exp_ext a; auto with sc].
  - ho_exp a0 P. rename P1 into P'. ho_exp a0 Q. rename Q1 into Q'.
    change ((fun a ⇒ nu (fun x : name ⇒ P' a x // Q' a x)) a0 = P0 a0) in HeqPa.
    auto_proc_ext.
    destruct (dec_name a0 a); subst.
    + change_ext. apply sc_scope. intros.
      fresh_lp (a0::b::a::nil) (nu (Q' a)).
      apply notin_arg with x; auto with hopi. solve_notin_rename.
    + change_ext. apply sc_scope. intros.
      fresh_lp (a0::b::a::nil) (nu (Q' a0)).
      apply notin_arg with x; auto. solve_notin_rename.
  - ho_exp a0 P. rename P1 into P'. ho_exp a0 Q. rename Q1 into Q'.
    change_ext. destruct (dec_name a0 a); subst.
    + change_ext. apply sc_scope_rev. intros.
      fresh_lp (a0::b::a::nil) (nu (Q' a)).
      apply notin_arg with x; auto with hopi. solve_notin_rename.
    + change_ext. apply sc_scope_rev. intros.
      fresh_lp (a0::b::a::nil) (nu (Q' a0)).
      apply notin_arg with x; auto. solve_notin_rename.
  - ho_ho_exp a P.
    change (( fun a ⇒ nu (fun x : name ⇒ nu (fun y : name ⇒ P1 a x y))) a = P0 a) in HeqPa.
    auto_proc_ext.
    change (( fun a ⇒ nu (fun y : name ⇒ nu (fun x : name ⇒ P1 a x y))) a = Q a) in HeqQa.
    auto_proc_ext; constructor.
  - exp_ext a. constructor. eapply IHHsc1; eauto. eapply IHHsc2; eauto.
  - destruct (dec_name a a0); subst; exp_ext a0;
      constructor; eapply IHHsc; eauto.
  - destruct (dec_name a a0); subst; exp_ext a0;
      (constructor; [eapply IHHsc1; eauto | eapply IHHsc2; eauto]).
  - ho_exp a P. ho_exp a Q. repeat change_ext.
    apply sc_nu with (a::L). intros c ?. simpl_notin.
    change (struct_congr ((fun b ⇒ (P1 b c)) b) ((fun b ⇒ (Q1 b c)) b)).
    apply H0 with c a; auto with hopi.
  - all_exp a.
    apply sc_trans with (Q1 b). eapply IHHsc1; eauto. eapply IHHsc2; eauto.
Qed.

Lemma sc_nuCF_newC_F : ∀ C C' F,
  conc_new C C' → (∀ a, notin_ho a F → notin a (F a)) → ∀ a,
  struct_congr (nu (fun x0 : name ⇒ appl (C x0) (F x0))) (appl C' (F a)).
Proof.
  intros. induction H.
  - simpl. apply sc_nu with (@nil name). intros. constructor×.
    apply sc_bind; auto with sc. fresh_proc (nu F).
    erewrite unused_arg; eauto.
  - simpl. fresh_proc (nu P).
    forwards*: H x. rewrite (unused_arg P x H1 a0 a).
    change (struct_congr (nu (fun x0 : name ⇒ Q x0 // subst (F x0) (P x0)))
      ((nu Q) // (fun x ⇒ subst (F x) (P x)) a)).
    clears x. apply sc_scope; intros.
    fresh_lp (a1::nil) ((nu F) // shiftV (nu P)).
    forwards*: H1 x. apply notin_bind_rev in H3.
    destruct H3. apply notin_bind.
    intros [|]; intros; simpl; auto with hopi.
    forwards*: H3 (@VZ Empty_set).
    apply isinV_rename with a1; auto. simpl in H8.
    fresh_proc (nu P). forwards*: H x0.
    rewrite (unused_arg P x0 H9 a1 x); auto.
    fresh_proc (nu F). forwards*: H0 x0.
    rewrite (unused_arg F x0 H7 a1 x); auto.
  - simpl. apply sc_trans with
      (nu (fun x ⇒ nu (fun x0 : name ⇒ appl (C x0 x) (F x0))));
      auto with sc.
    fn (conc_nu (fun y ⇒ conc_nu (fun x ⇒ C y x))).
    apply sc_nu with (L++L0). intros.
    change (struct_congr
      ((fun a0 ⇒ nu (fun x0 : name ⇒ appl (C x0 a0) (F x0))) a0)
      ((fun a0 ⇒ appl (C' a0) (F a)) a0)).
    apply× H1; simpl_notin.
    forwards*: H2 a0. simpl_notin.
Qed.

Lemma sc_nuFC_nuF_C' : ∀ n C', sizec C' n →
  ∀ C c, (conc_notin_ho c C) → C' = (C c) →
  (∀ a, conc_notin_ho a C → conc_notin a (C a)) → ∀ a F,
  struct_congr (nu (fun x ⇒ appr (F x) (C x))) (appr (nu F) (C a)).
Proof.
  induction n; introv Hs; inverts Hs; intros.
  + conc_exp_ext c.
    fresh_proc ((nu P0) // nu Q0).
    forwards*: H1 x. auto with hopi. inverts H0.
    apply sc_trans with
    ((nu (fun x : name ⇒ subst (F x) (P0 x))) // Q0 a).
    constructor. eapply notin_arg; eauto.
    constructor; auto with sc.
    apply sc_nu with (@nil name). intros.
    apply sc_bind; auto with sc. intros [|]; simpl; auto with sc.
    rewrite (unused_arg P0 x H9 a0 a). auto with sc.
  + destruct (conc_ho_beta_exp c C) as [C' [HC']]; subst.
    conc_change_ext. apply sc_trans with
    (nu (fun x0 ⇒ nu (fun x ⇒ appr (F x) (C' x x0)))); auto with sc.
    apply sc_nu with (c::nil). intros.
    change (struct_congr (
      nu (fun x0 ⇒ appr (F x0) ((fun y ⇒ C' y a0) x0)))
      (appr (nu F) ((fun x0 ⇒ C' x0 a0) a))).
    eapply IHn; eauto.
    intros_all. forwards*: HC' b. inverts× H4.
    eapply conc_notin_rename; eauto. simpl_notin.
    intros. forwards*: H2 a1. intros_all. constructor; intros.
    forwards*: H3 b. eapply conc_notin_rename; eauto.
    inverts H4. destruct (dec_name a1 a0); subst; auto.
    apply× two_unused_args.
Qed.

Lemma sc_nuFC_nuF_C : ∀ F C,
  (∀ a, conc_notin_ho a C → conc_notin a (C a)) → ∀ a,
  struct_congr (nu (fun x ⇒ appr (F x) (C x))) (appr (nu F) (C a)).
Proof.
  intros. fresh_conc (conc_nu C).
  destruct (exists_szc (C x)) as [n].
  eapply sc_nuFC_nuF_C'; eauto.
Qed.

Lemma sc_F_newPC_F_nuP_C' : ∀ n C'', sizec C'' n →
  ∀ C' c, (conc_notin_ho c C') → C'' = (C' c) →
  ∀ F C P,
  conc_new (fun x ⇒ conc_parr (P x) (C' x)) C →
  (∀ a, conc_notin_ho a C' → conc_notin a (C' a)) → ∀ a,
  struct_congr (appr F C) (appr F (conc_parr (nu (fun x0 ⇒ (P x0))) (C' a))).
Proof.
  induction n; intros; inverts H; simpl.
  - conc_exp_ext c. inverts H2.
    + assert (P0 = P1). fun_eq_solve.
      assert (Q = fun x ⇒ P x // Q0 x). fun_eq_solve.
      subst. fresh_conc (conc_nu (fun x ⇒ conc_def (P1 x)(Q0 x))).
      forwards*: H8 x. intros_all. forwards*: H11 b. simpl_notin.
      forwards*: H3 x. simpl_notin. exfalso.
      forwards*: @sep x x.
    + assert (P0 = P1). fun_eq_solve.
      assert (Q = fun x ⇒ P x // Q0 x). fun_eq_solve.
      subst. simpl. constructor.
      asserts_rewrite (P1 a0 = P1 a).
      fresh_proc (nu P1). apply unused_arg with x. apply× H8.
      auto with sc.
      apply sc_scope; intros.
      fresh_conc (conc_nu (fun x ⇒ conc_def (P1 x)(Q0 x))).
      forwards*: H3 x. simpl_notin. eapply notin_arg; eauto.
    + fun_eq_absurd.
  - destruct (conc_ho_beta_exp c C0) as [C'' [HC'']]; subst.
    conc_change_ext. inverts H2; try fun_eq_absurd.
    assert (C0 = fun x ⇒ fun x0 ⇒ conc_parr (P x) (C'' x x0)).
      extens; intros. apply equal_f with x1 in H.
      inverts H. apply equal_f with x2 in H4; auto.
    fn (conc_nu (fun x0 ⇒ conc_nu (fun x1 ⇒ conc_parr (P x0) (C'' x0 x1)))).
    subst. simpl. apply sc_nu with (c::(L++L0)); intros.
    change (struct_congr (appr F (C' a0))
      (appr F (conc_parr (nu (fun x0 ⇒ P x0)) ((fun a ⇒ (C'' a a0)) a)))).
    eapply IHn; eauto.
    intros_all. forwards*: H0 b. simpl_notin.
    apply× H1; simpl_notin. forwards*: H4 a0; simpl_notin.
    intros. forwards*: H3 a1. intros_all.
    constructor; intros. forwards*: H5 b.
    eapply conc_notin_rename; eauto.
    simpl_notin. destruct (dec_name a0 a1); auto.
    subst. apply× two_unused_args.
Qed.

Lemma sc_F_newPC_F_nuP_C : ∀ F C' C P,
  conc_new (fun x ⇒ conc_parr (P x) (C' x)) C →
  (∀ a, conc_notin_ho a C' → conc_notin a (C' a)) → ∀ a,
  struct_congr (appr F C) (appr F (conc_parr (nu (fun x0 ⇒ (P x0))) (C' a))).
Proof.
  intros. fresh_conc (conc_nu C').
  destruct (exists_szc (C' x)) as [n].
  eapply sc_F_newPC_F_nuP_C'; eauto.
Qed.

Lemma sc_F_newCQ_F_newC_Q' : ∀ n C0, sizec C0 n →
  ∀ C' c, (conc_notin_ho c C') → C0 = (C' c) →
  ∀ F C C'' Q,
  (∀ a : name, notin_ho a Q → notin a (Q a)) →
  conc_new (fun x : name ⇒ conc_parl (C' x) (Q x)) C →
  conc_new C' C'' → ∀ a,
  struct_congr (appr F C) (appr F (conc_parl C'' (Q a))).
Proof.
  induction n; intros; inverts H; simpl.
  - conc_exp_ext c. inverts H4; try fun_eq_absurd.
    + assert(P=P0). fun_eq_solve.
      assert (Q0=Q1). fun_eq_solve. subst.
      inverts H3; try fun_eq_absurd.
      × assert(P=P0). fun_eq_solve.
        assert (Q0 = fun x ⇒ (Q1 x // Q x)). fun_eq_solve.
        subst. simpl. apply sc_nu with (@nil name); intros.
        repeat constructor; auto with sc.
        fresh_proc (nu Q).
        rewrite (unused_arg Q x (H2 x H14) a0 a); eauto.
      × assert (P=P0). fun_eq_solve. subst.
        fresh_proc (nu P0). forwards*: H12 x.
        forwards*: H10 x. exfalso. forwards*: @sep x x.
    + assert(P=P0). fun_eq_solve.
      assert (Q0=Q1) by fun_eq_solve. subst.
      inverts H3; try fun_eq_absurd.
      × assert (P=P0) by fun_eq_solve. subst.
        fresh_proc (nu P0). forwards*: H12 x.
        forwards*: H10 x. exfalso. forwards*: @sep x x.
      × assert(P=P0) by fun_eq_solve.
        assert (Q0 = fun x ⇒ (Q1 x // Q x)) by fun_eq_solve.
        subst. simpl. constructor.
        rewrite (unused_arg P0 c (H12 c H6) a1 a0). auto with sc.
        apply sc_scope; auto.
  - destruct (conc_ho_beta_exp c C1) as [C1' [HC1']]; subst.
    conc_change_ext. inverts H4; try fun_eq_absurd.
    assert (C0 = C1') by fun_eq_solve. subst.
    inverts H3; try fun_eq_absurd.
    assert (C0 = fun x ⇒ fun x0 ⇒ conc_parl (C1' x x0) (Q x)).
      extens; intros. apply equal_f with x1 in H4.
      inverts H4. apply equal_f with x2 in H6. auto.
    subst. simpl.
    fn((conc_nu (fun b ⇒ conc_nu (fun x0 : name ⇒ conc_parl (C1' b x0) (Q b))))).
    apply sc_nu with (c::(L++L0++L1)); intros.
    simpl_notin. forwards*: H3 a0.
    change (struct_congr (appr F (C'0 a0))
      (appr F (conc_parl (C' a0) ((fun a ⇒ (Q a)) a)))).
    eapply IHn. 5:{ apply× H5. simpl_notin. }
      5:{ apply× H1. intros_all. simpl_notin.
          forwards*: H15 b. inverts H11.
          constructor; intros. forwards*: H16 b0.
          apply nc_parl in H13. intuition. }
      apply H7. 2:{ simpl. reflexivity. }
      intros_all. forwards*: H0 b. inverts× H13.
      auto.
Qed.

Lemma sc_F_newCQ_F_newC_Q : ∀ F C C' C'' Q,
  (∀ a : name, notin_ho a Q → notin a (Q a)) →
  conc_new (fun x : name ⇒ conc_parl (C' x) (Q x)) C →
  conc_new C' C'' → ∀ a,
  struct_congr (appr F C) (appr F (conc_parl C'' (Q a))).
Proof.
  intros. fresh_conc (conc_nu C').
  destruct (exists_szc (C' x)) as [n].
  eapply sc_F_newCQ_F_newC_Q'; eauto.
Qed.


Lemma sc_FP_C_FC_P : ∀ F C P,
  struct_congr (appr (abs_parl F P) C)(appr F C // P).
Proof.
  induction C; simpl; intros.
  + rewrite subst_shift. eauto with sc.
  + apply sc_trans with (nu (fun x ⇒ (appr F (c x) // P))).
    apply sc_nu with (@nil name); intros.
    auto with sc.
    fresh_list (@nil name).
    change (struct_congr (nu (fun x0 ⇒ appr F (c x0) // (fun _ ⇒ P) x0))
      ((nu (fun x0 : name ⇒ appr F (c x0))) // (fun _ ⇒ P) x)).
    apply sc_scope; auto with hopi. intros_all. fresh_list (a::nil).
    forwards*: H0 x0.
Qed.

Lemma sc_PF_C_FC_P : ∀ F C P,
  struct_congr (appr (abs_parr P F) C)(appr F C // P).
Proof.
  induction C; simpl; intros.
  + rewrite subst_shift. eauto with sc.
  + apply sc_trans with (nu (fun x ⇒ (appr F (c x) // P))).
    apply sc_nu with (@nil name); intros.
    auto with sc.
    fresh_list (@nil name).
    change (struct_congr (nu (fun x0 ⇒ appr F (c x0) // (fun _ ⇒ P) x0))
      ((nu (fun x0 : name ⇒ appr F (c x0))) // (fun _ ⇒ P) x)).
    apply sc_scope; auto with hopi. intros_all. fresh_list (a::nil).
    forwards*: H0 x0.
Qed.

Lemma sc_F_PC_FC_P : ∀ F C P,
  struct_congr (appr F (conc_parl C P))(appr F C // P).
Proof.
  induction C; simpl; intros.
  + eauto with sc.
  + apply sc_trans with (nu (fun x ⇒ (appr F (c x) // P))).
    apply sc_nu with (@nil name); intros.
    auto with sc.
    fresh_list (@nil name).
    change (struct_congr (nu (fun x0 ⇒ appr F (c x0) // (fun _ ⇒ P) x0))
      ((nu (fun x0 : name ⇒ appr F (c x0))) // (fun _ ⇒ P) x)).
    apply sc_scope; auto with hopi. intros_all. fresh_list (a::nil).
    forwards*: H0 x0.
Qed.

Lemma sc_F_CP_FC_P : ∀ F C P,
  struct_congr (appr F (conc_parr P C))(appr F C // P).
Proof.
  induction C; simpl; intros.
  + eauto with sc.
  + apply sc_trans with (nu (fun x ⇒ (appr F (c x) // P))).
    apply sc_nu with (@nil name); intros.
    auto with sc.
    fresh_list (@nil name).
    change (struct_congr (nu (fun x0 ⇒ appr F (c x0) // (fun _ ⇒ P) x0))
      ((nu (fun x0 : name ⇒ appr F (c x0))) // (fun _ ⇒ P) x)).
    apply sc_scope; auto with hopi. intros_all. fresh_list (a::nil).
    forwards*: H0 x0.
Qed.

Hint Resolve sc_FP_C_FC_P sc_PF_C_FC_P sc_F_CP_FC_P sc_F_PC_FC_P:sc.


Lemma sc_nuF_C_nuFC : ∀ C F,
struct_congr (appr (nu F) C)(nu (fun x ⇒ appr (F x) C)).
Proof.
  induction C; intros; simpl; eauto with sc.
  fresh_list (@nil name).
  change (struct_congr ((nu (fun x : name ⇒ subst (F x) p)) // (fun _ ⇒ p0) x)
      (nu (fun x : name ⇒ subst (F x) p // (fun _ ⇒ p0) x))).
  apply sc_scope_rev; intros; auto with hopi.
  fresh_list (a::nil). forwards*: H x0.
  Unshelve. exact (@nil name).
Qed.

Lemma sc_F_nuC_nuFC : ∀ C C' F, conc_new C' C →
struct_congr (appr F C)(nu (fun x ⇒ appr F (C' x))).
Proof.
  intros. gen F. induction H; intros; simpl; eauto with sc.
  apply sc_trans with ((nu Q) // subst F (P a)); auto with sc.
  apply sc_trans with ((nu (fun x ⇒ Q x // subst F (P x)))); eauto with sc.
  change (struct_congr ((nu Q) // (fun x ⇒ (subst F (P x))) a)
        (nu (fun x : name ⇒ Q x // subst F (P x)))).
  apply sc_scope_rev; intros.
  fresh_list (a0::a::nil). forwards*: H0 x.
  apply notin_bind_rev in H3. destruct_hyps.
  apply× @notin_bind. intros [|]; simpl; auto with hopi.
  intros. forwards*: H3. simpl_notin. apply H. intros_all.
  eapply notin_rename; eauto.

  apply sc_trans with
    (nu (fun x0 ⇒ nu (fun x ⇒ appr F (C x x0)))); auto with sc.
  fn (conc_nu (fun x ⇒ conc_nu (fun y ⇒ C x y))).
  apply sc_nu with (L++L0); intros. simpl_notin.
  forwards*: H1. apply× H0.
  intros_all. constructor; intros. simpl_notin.
  forwards*: H9 b; simpl_notin.
  Unshelve. exact (@nil name).
Qed.

Hint Resolve sc_nuF_C_nuFC sc_F_nuC_nuFC:sc.

Ltac auto_sc_nu := try apply sc_nu with (@nil name); auto with sc.

Ltac simpl_lts :=
  simpl in *; repeat match goal with
  | [ H : ltsproc ?t _ |- _ ] ⇒ head_constructor t; inverts H
  | [ H : ltsabs ?t _ _ |- _ ] ⇒ head_constructor t; inverts H
  | [ H : ltsconc ?t _ _ |- _ ] ⇒ head_constructor t; inverts H
  end.

Ltac ind_conc :=
  match goal with
  | C: conc |- _ ⇒
    repeat match goal with
    | H: context [ C ] |- _ ⇒ clear H
    end; induction C
  end.

Lemma struct_congr_sim' {V : Set} : ∀ P Q f, @struct_congr V P Q →
  ∀ P', P' = (mapV f P) →
  test_proc struct_congr P' (mapV f Q) ∧
  test_abs struct_congr P' (mapV f Q) ∧
  test_conc struct_congr P' (mapV f Q).
Proof.
  intros P Q f Hstruct. induction Hstruct using struct_congr_ind'; intros P'' Hp''; subst.
  +
    splits; introv Hlts; intros;
    simpl_lts; eexists; split; eauto with hopi;
    try solve [simpl; auto with sc];
    try solve [ind_conc; simpl; auto_sc_nu].
    -
      ind_conc; simpl; auto with sc.
      apply sc_trans with (nu (fun x ⇒ (mapV f P // appl (c x) F))); auto_sc_nu.
      apply sc_trans with ((nu (fun x : name ⇒ appl (c x) F)) // mapV f P); auto with sc.
      apply sc_trans with (nu (fun x : name ⇒ appl (c x) F // mapV f P)); auto_sc_nu.
      change (struct_congr ((nu (fun x : name ⇒ appl (c x) F)) // (fun x ⇒ mapV f P) a)
                                (nu (fun x : name ⇒ appl (c x) F // (fun x ⇒ mapV f P) x))).
      apply sc_scope_rev. intros. fresh_list (a0::nil). forwards*: H0 x.
    -
      ind_conc; simpl.
      rewrite subst_shift; auto with sc.
      apply sc_trans with (nu (fun x ⇒ (mapV f P // appr F (c x)))); auto_sc_nu.
      apply sc_trans with ((nu (fun x : name ⇒ appr F (c x))) // mapV f P); auto with sc.
      apply sc_trans with (nu (fun x : name ⇒ appr F (c x) // mapV f P)); auto_sc_nu.
      change (struct_congr ((nu (fun x : name ⇒ appr F (c x))) // (fun x ⇒ mapV f P) a)
                                (nu (fun x : name ⇒ appr F( c x) // (fun x ⇒ mapV f P) x))).
      apply sc_scope_rev. intros. fresh_list (a0::nil). forwards*: H0 x.
    -
      ind_conc; simpl.
      rewrite subst_shift; auto with sc.
      apply sc_trans with ((nu (fun x : name ⇒ appl (c x) F0 // mapV f R))); auto_sc_nu.
      change (struct_congr (nu (fun x : name ⇒ appl (c x) F0 // (fun x ⇒ mapV f R) x))
             ((nu (fun x : name ⇒ appl (c x) F0)) // (fun x ⇒ mapV f R) a)).
      apply sc_scope. intros. fresh_list (a0::nil). forwards*: H0 x.
    -
      eauto with sc.
    -
      eauto with sc.
  +
    splits; introv Hlts; intros;
    simpl_lts; eexists; split; eauto with hopi;
    try solve [simpl; auto with sc];
    try solve [ind_conc; simpl; auto_sc_nu].
    -
      eauto with sc.
    -
      eauto with sc.
    -
      eauto with sc.
    -
      eauto with sc.
    -
      eauto with sc.
  +
    splits; introv Hlts; intros;
    simpl_lts; eexists; split; eauto with hopi;
    try solve [simpl; auto with sc];
    try solve [ind_conc; simpl; auto_sc_nu].
  +
    splits; introv Hlts; intros;
    simpl_lts; eexists; split; eauto with hopi;
    try solve [simpl; auto with sc];
    try solve [ind_conc; simpl; auto_sc_nu].
  +
    splits; introv Hlts; intros;
    simpl_lts; eexists; split; eauto with hopi;
    try solve [simpl; auto with sc];
    try solve [ind_conc; simpl; auto_sc_nu].
  +
    splits; introv Hlts; intros; simpl_lts.
    - fresh_lp (a::L) (mapV f ((nu P) // nu Q) // nu P').
      forwards*: H1 x. auto with hopi. inverts H2.
      ×
        all_exp x. rename P'1 into P''.
        ∃ ((nu P'') // mapV f (Q a)). split.
        apply ltsp_parl. apply ltsp_new with (x::L); intros.
        change (ltsproc ((fun a0 ⇒ mapV f (P a0)) a0) (P'' a0)).
        apply ltsproc_rename with x; auto with hopi.
        change_ext.
        change (struct_congr (nu (fun x0 : name ⇒ P'' x0 // mapV f (Q x0)))
          ((nu P'') // ((fun x ⇒ mapV f (Q x)) a))).
        apply sc_scope; intros. auto with hopi.
     ×
        destruct (beta_exp x P'0) as [Q''].
        destruct_hyps; subst.
        ∃ ((nu (fun x0 ⇒ mapV f (P x0))) // Q'' a). split.
        apply ltsp_parr.
        change (ltsproc ((fun a0 ⇒ mapV f (Q a0)) a) (Q'' a)).
        apply ltsproc_rename with x; auto with hopi.
        change_ext. apply sc_scope. apply ltsproc_unused_arg with
            (fun x ⇒ mapV f (Q x)) x; auto with hopi.
     ×
        destruct (beta_exp x F) as [F'].
        destruct (conc_beta_exp x C) as [C'].
        destruct_hyps; subst.
        destruct (exists_cnew C') as [C''].
        ∃ (appl C'' (F' a)). split.
        assert (a0 ≠ x).
        apply ltsabs_notin_label with (mapV f (Q x)) (F' x); auto with hopi.
        change (ltsabs ((fun x ⇒ mapV f (Q x)) x) a0 (F' x)) in H11.
        assert (subst_name x a a0 a0). constructor×.
        eapply ltsabs_rename in H11; eauto.
        eapply lts_taul'; eauto.
        apply ltsc_new with C' (x::a0::L); auto; intros.
        change (ltsconc ((fun x ⇒ mapV f (P x)) b) a0 (C' b)).
        apply ltsconc_rename with a0 x; auto. constructor×.
        change_ext. apply× sc_nuCF_newC_F.
        apply ltsabs_unused_arg with ((fun x ⇒ mapV f (Q x))) x a0; auto with hopi.
      ×
        destruct (beta_exp x F) as [F'].
        destruct (conc_beta_exp x C) as [C'].
        destruct_hyps; subst.
        ∃ (appr (nu F') (C' a)). split.
        assert (a0 ≠ x).
        apply ltsconc_notin_label with (mapV f (Q x)) (C' x); auto with hopi.
        change (ltsconc ((fun x ⇒ mapV f (Q x)) x) a0 (C' x)) in H11.
        assert (subst_name x a a0 a0). constructor×.
        eapply ltsconc_rename in H11; eauto.
        eapply lts_taur'; eauto.
        apply ltsa_new with (a0::x::L); intros.
        change (ltsabs ((fun x ⇒ mapV f (P x)) b) a0 (F' b)).
        apply ltsabs_rename with a0 x; auto. constructor×.
        change_ext. apply× sc_nuFC_nuF_C.
        apply ltsconc_unused_arg with (fun x ⇒ mapV f (Q x)) x a0; eauto; auto with hopi.
    - fresh_lp (a::a0::L) (shiftV (mapV f ((nu P) // nu Q)) // nu F0).
      assert (∀ z : name, z ≠ x → notin x (mapV f (Q z))) by
        eauto using notin_mapV_rev.
      assert (∀ z : name, z ≠ x → notin x (mapV f (P z))) by
        eauto using notin_mapV_rev.
      clear H8 H7. forwards*: H2 x. auto with hopi. inverts H7.
      ×
        destruct (beta_exp x F) as [F']. destruct_hyps; subst.
        ∃ (abs_parl (nu F') (mapV f (Q a))). split.
        apply ltsa_parl. apply ltsa_new with (x::a::a0::L); intros.
        change (ltsabs ((fun b ⇒ mapV f (P b)) b) a0 (F' b)).
        apply ltsabs_rename with a0 x; eauto with hopi.
        change_ext. ind_conc; simpl; auto_sc_nu. constructor; auto with sc.
        rewrite subst_shift.
        apply sc_trans with
            (nu (fun x0 : name ⇒ subst (F' x0) p // (mapV f (Q x0)))).
          { auto_sc_nu. intros. rewrite subst_shift; auto with sc. }
        change (struct_congr (nu (fun x0 : name ⇒ subst (F' x0) p // mapV f (Q x0)))
               ((nu (fun x0 : name ⇒ subst (F' x0) p)) // (fun x ⇒ mapV f (Q x)) a)).
        apply sc_scope; intros. auto with hopi.
      ×
        destruct (beta_exp x F) as [F']. destruct_hyps; subst.
        ∃ (abs_parr (nu (fun x0 ⇒ mapV f (P x0))) (F' a)). split.
        apply ltsa_parr.
        change (ltsabs ((fun b ⇒ mapV f (Q b)) a) a0 (F' a)).
        apply ltsabs_rename with a0 x; eauto with hopi.
        change_ext. ind_conc; simpl; auto_sc_nu. constructor; auto with sc.
        change (struct_congr
  (nu (fun x0 : name ⇒ subst (shiftV (mapV f (P x0))) p // subst (F' x0) p))
  ((nu (fun x0 : name ⇒ subst (shiftV (mapV f (P x0))) p)) //
    (fun x ⇒ subst (F' x) p) a)).
        apply sc_scope. intros. apply notin_bind.
        intros [|]; simpl; auto with hopi. intros.
        fresh_lp (a1::x::L) (shiftV p // (nu F')).
        forwards*: H0 x0. apply notin_bind_rev in H11.
        destruct_hyps. forwards*: H11 (@VZ Empty_set).
        eapply isinV_rename; eauto.
        change (ltsabs ((fun x ⇒ (mapV f (Q x))) x) a0 (F' x)) in H12.
        assert (∀ a, notin_ho a F' → notin a (F' a)).
          apply ltsabs_unused_arg with (fun x ⇒ mapV f (Q x)) x a0; auto with hopi.
        auto with hopi.
    - fresh_lpc (a::a0::L) (mapV f (nu P) // mapV f (nu Q)) (conc_nu C0).
      forwards*: H1 x. auto with hopi. inverts H3.
      ×
        destruct (conc_beta_exp x C1) as [C'].
        destruct_hyps; subst.
        destruct (exists_cnew C') as [C''].
        ∃ (conc_parl C'' (mapV f (Q a))). split.
        apply ltsc_parl. apply ltsc_new with C' (x::a::a0::L); auto; intros.
        change (ltsconc ((fun b ⇒ mapV f (P b)) b) a0 (C' b)).
        apply ltsconc_rename with a0 x; eauto. constructor×.
        conc_change_ext.
        change (struct_congr (appr F C)
          (appr F (conc_parl C'' ((fun a ⇒ mapV f (Q a)) a)))).
        eapply sc_F_newCQ_F_newC_Q; eauto; auto with hopi.
     ×
        destruct (conc_beta_exp x C1) as [C']. destruct_hyps; subst.
        ∃ (conc_parr (nu (fun x0 ⇒ mapV f (P x0))) (C' a)). split.
        apply ltsc_parr.
        change (ltsconc ((fun b ⇒ mapV f (Q b)) a) a0 (C' a)).
        apply ltsconc_rename with a0 x; eauto. constructor×.
        conc_change_ext. apply× sc_F_newPC_F_nuP_C.
        apply ltsconc_unused_arg with (fun x ⇒ mapV f (Q x)) x a0; auto with hopi.
  +
    splits; introv Hlts; simpl_lts; intros.
      ×
        ∃ (nu (fun x ⇒ P'0 x // mapV f (Q x))); split.
        apply ltsp_new with (a::L); intros. constructor.
        simpl_notin. eapply H2; eauto with hopi.
        change (struct_congr ((nu P'0) // (fun x ⇒ mapV f (Q x)) a)
            (nu (fun x : name ⇒ P'0 x // mapV f (Q x)))).
        auto with sc hopi.
     ×
       all_exp a. ∃ (nu (fun x ⇒ mapV f (P x) // P'0 x)); split.
        apply ltsp_new with (a::nil); intros. constructor×.
        change (ltsproc ((fun a0 ⇒ mapV f (Q a0)) a0) (P'0 a0)).
        apply ltsproc_rename with a; simpl_notin; auto with hopi.
        change (struct_congr ((nu (fun x ⇒ mapV f (P x))) // (fun x ⇒ P'0 x) a)
            (nu (fun x : name ⇒ mapV f (P x) // P'0 x))).
        apply sc_scope_rev; intros.
        apply ltsproc_unused_arg with (fun x ⇒ mapV f (Q x)) a; auto with hopi.
     ×
       all_exp a. ∃ (nu (fun x ⇒ appl (C0 x)(F0 x))). split.
       fn (conc_nu C0).
       apply ltsp_new with (a0::(L++L0)); intros. simpl_notin.
       eapply lts_taul'; eauto with hopi. apply× H2.
       auto with hopi. forwards*: H3 a1. simpl_notin.
       change (ltsabs ((fun x ⇒ mapV f (Q x)) a1) a0 (F0 a1)).
       eapply ltsabs_rename; eauto with hopi. constructor×.
       eapply ltsabs_notin_label; eauto with hopi.
       apply sc_symmetric. apply× sc_nuCF_newC_F.
       change (ltsabs ((fun x ⇒ mapV f (Q x)) a) a0 (F0 a)) in H5.
       eapply ltsabs_unused_arg; eauto; auto with hopi.
     ×
       all_conc_exp a. ∃ (nu (fun x ⇒ appr (F0 x)(C0 x))); split.
       fn (nu F0).
       apply ltsp_new with (a0::(L++L0)); intros. simpl_notin.
       eapply lts_taur'; eauto with hopi.
       2:{ apply× H2. auto with hopi. forwards*: H3 a1. simpl_notin. }
       change (ltsconc ((fun x ⇒ mapV f (Q x)) a1) a0 (C0 a1)).
       eapply ltsconc_rename; eauto with hopi. constructor×.
       eapply ltsconc_notin_label; eauto with hopi.
       apply sc_symmetric. apply× sc_nuFC_nuF_C.
       change (ltsconc ((fun x ⇒ mapV f (Q x)) a) a0 (C0 a)) in H5.
       eapply ltsconc_unused_arg; eauto; auto with hopi.
     ×
       ∃ (nu (fun x ⇒ abs_parl (F x)(mapV f (Q x)))). split.
       fn (nu F). apply ltsa_new with (a0::(L++L0)); intros; simpl_notin.
       constructor. apply H2; auto with hopi. forwards*: H3 b; simpl_notin.
       apply sc_symmetric. ind_conc; simpl; auto with sc.
       constructor; auto with sc. change (struct_congr
  (nu (fun x ⇒ subst (F x) p // subst (shiftV (mapV f (Q x))) p))
  ((nu (fun x ⇒ subst (F x) p)) // (fun a ⇒ subst (shiftV (mapV f (Q a))) p) a)).
       apply sc_scope; intros. rewrite subst_shift. auto with hopi.
       apply sc_nu with L; auto.
     ×
       all_exp a. ∃ (nu (fun x ⇒ abs_parr (mapV f (P x))(F1 x))). split.
       fn (nu F1). apply ltsa_new with (a0::(L++L)); intros; simpl_notin.
       constructor. change (ltsabs ((fun x ⇒ mapV f (Q x)) b) a0 (F1 b)).
       eapply ltsabs_rename; eauto; auto with hopi. constructor×.
       eapply ltsabs_notin_label; eauto with hopi.
       ind_conc; simpl; auto with sc.
       constructor; auto with sc. change (struct_congr
  ((nu (fun x ⇒ subst (shiftV (mapV f (P x))) p)) // (fun a ⇒ subst (F1 a) p) a)
  (nu (fun x ⇒ subst (shiftV (mapV f (P x))) p // subst (F1 x) p))).
       apply sc_scope_rev; intros.
       fresh_lp (a1::nil) p. forwards*: H1 x.
       apply notin_bind_rev in H6. intuition. apply notin_bind.
       intros [|]; simpl; auto with hopi. intros.
       forwards*: H7 (@VZ Empty_set). eapply isinV_rename; eauto.
       apply ltsabs_unused_arg with (fun x ⇒ mapV f (Q x)) a a0; auto with hopi.
       apply sc_nu with (a::nil); auto.
     ×
       destruct (exists_cnew (fun x ⇒ conc_parl (C x)(mapV f (Q x)))) as [C'].
       ∃ C'. split.
       fn (conc_nu C). apply ltsc_new with
        (fun x : name ⇒ conc_parl (C x) (mapV f (Q x))) (a0::(L++L0));
        intros; simpl_notin.
       constructor. apply H2; auto with hopi. forwards*: H4 b; simpl_notin.
       apply sc_symmetric.
       change (struct_congr (appr F C')
              (appr F (conc_parl C0 ((fun a ⇒ mapV f (Q a)) a)))).
       eapply sc_F_newCQ_F_newC_Q; eauto. intros; auto with hopi.
     ×
       all_conc_exp a.
       destruct (exists_cnew (fun x ⇒ conc_parr (mapV f (P x)) (C1 x))) as [C'].
       ∃ C'. split.
       apply ltsc_new with
        (fun x : name ⇒ conc_parr (mapV f (P x))(C1 x) ) (a0::nil);
        intros; simpl_notin.
       constructor. change (ltsconc ((fun b ⇒ mapV f (Q b)) b) a0 (C1 b)).
       eapply ltsconc_rename; eauto with hopi. constructor.
       eapply ltsconc_notin_label; eauto with hopi.
       apply sc_symmetric. apply× sc_F_newPC_F_nuP_C.
       change (ltsconc ((fun x ⇒ mapV f (Q x)) a) a0 (C1 a)) in H5.
       eapply ltsconc_unused_arg; eauto; auto with hopi.
  + splits; introv Hlts; intros;
    simpl_lts.
    - fresh_lp L (nu P'). forwards*: H0 x.
      intros_all. auto with hopi. simpl_lts.
    - fresh_lp (a::L) (nu F0) . forwards*: H1 x.
      intros_all. auto with hopi. simpl_lts.
    - fresh_lc (a::L) (conc_nu C0). forwards*: H0 x.
      intros_all. auto with hopi. simpl_lts.
  + splits; introv Hlts; intros; simpl_lts.
  +
    splits.
    × introv Hlts. simpl_lts.
      fresh_lp L ((nu (fun x0 : name ⇒ nu (fun x1 : name ⇒ mapV f (P x0 x1)))) // nu P').
      forwards*: H0 x. rename H0 into HLTS. simpl_lts.
      destruct (ho_beta_exp x P'0) as [P'' [HxP'']]; subst.
      change ((fun x ⇒ nu P'' x) x = P' x) in H4. auto_proc_ext. clears x.
      ∃ (nu (fun x1 : name ⇒ nu (fun x2 : name ⇒ (P'' x2 x1)))).
      split; auto with sc.
      apply ltsp_new with L. intros a HaL Ha1 Ha2.
      apply ltsp_new with L. intros b HbL Hb1 Hb2.
      forwards: HLTS b; auto.
      { intros y Hy. forwards*: Hb1 y. constructor. intros z Hz.
        change (notin b ((fun z ⇒ mapV f (P y z)) z)). eapply notin_rename; eauto. }
      { intros y Hy. forwards*: Hb2 y. constructor. intros z Hz.
        change (notin b ((fun z ⇒ (P'' y z)) z)). eapply notin_rename; eauto. }
      simpl_lts.
      fresh_lp (a::b::L1) ((nu (fun x0 : name ⇒ mapV f (P b x0))) // nu (P'' b)).
      forwards Rbx: H2 x; auto.
      change (ltsproc ((fun x ⇒ mapV f (P b x)) a) (P'' b a)).
      apply ltsproc_rename with x; auto.
    × introv Hlts. simpl_lts.
      fresh_lp L ((pr_nu (fun x0 : name ⇒ nu (fun x1 : name ⇒ mapV f (P x0 x1))))
                    // (a ? pr_nu F0)).
      forwards*: H0 x. rename H0 into HLTS. simpl_lts.
      destruct (ho_beta_exp x F) as [F'' [HxF'']]; subst.
      change ((fun x ⇒ nu F'' x) x = F0 x) in H4. auto_proc_ext. clears x.
      ∃ (nu (fun x1 : name ⇒ nu (fun x2 : name ⇒ (F'' x2 x1)))).
      split; [| ind_conc; simpl; auto_sc_nu]. clears C L0.
      apply ltsa_new with L. intros b HbL Hab Hb1 Hb2.
      apply ltsa_new with L. intros c HcL Hac Hc1 Hc2.
      forwards: HLTS c; auto with hopi.
      { intros y Hy. forwards*: Hc1 y. constructor. intros z Hz.
        change (notin c ((fun z ⇒ mapV f (P y z)) z)). eapply notin_rename; eauto. }
      { intros y Hy. forwards*: Hc2 y. constructor. intros z Hz.
        eapply notin_rename; eauto. }
      simpl_lts.
      fresh_lp (b::c::L0) ((nu (fun x0 : name ⇒ mapV f (P c x0))) // (a ? nu (F'' c))).
      forwards Rbx: H3 x; auto.
      change (ltsabs ((fun x ⇒ mapV f (P c x)) b) a (F'' c b)).
      apply ltsabs_rename with a x; auto. constructor×.
    × introv Hlts. simpl_lts.
      fresh_lpc (a::L)(nu (fun x ⇒ nu (fun y ⇒ mapV f (P x y))))
                (conc_nu C0).
      forwards*: H0 x. inverts H2. ho_conc_exp x C1.
      fresh_lpc (a::L)(nu (fun x ⇒ nu (fun y ⇒ mapV f (P x y))))
                (conc_nu (fun x ⇒ conc_nu (fun y ⇒ C2 x y))).
      rename x0 into y.
      destruct (exists_cnew (fun x ⇒ C2 x y)) as [C''].
      conc_exp y C''. destruct (exists_cnew C''0) as [C'].
      intros. ∃ C'; split.
      fn(conc_nu (fun x ⇒ (conc_nu (fun y ⇒ C2 x y)))).
      apply ltsc_new with C''0 (a::x::L++L0++L1); auto; intros.
      simpl_notin.
      apply ltsc_new with (fun x ⇒ C2 x b)(a::b::x::L++L0++L1); auto; intros.
      simpl_notin. forwards*: H5 b.
        intros_all. forwards*: H18 b1. simpl_notin.
        intros_all. forwards*: H15 b. simpl_notin.
        forwards*: H37 x. simpl_notin.
      change (ltsconc ((fun b0 ⇒ mapV f (P b0 b)) b0) a ((fun b0 ⇒ C2 b0 b) b0)).
      assert (subst_name x b0 a a). constructor×.
      apply ltsconc_rename with a x; eauto; auto with hopi.
        intros_all. forwards*: H6 b1. simpl_notin.
      change (conc_new ((fun b ⇒ fun x0 : name ⇒ C2 x0 b) b) (C''0 b)).
      apply cnew_rename with y; eauto.
        intros_all. constructor. intros.
        forwards*: H14 b1. simpl_notin.
      apply sc_trans with (nu (fun y ⇒ appr F (C''0 y))); auto with sc.
      apply sc_trans with (nu (fun y ⇒ appr F (C0 y))); auto with sc.
      apply sc_trans with (nu (fun y ⇒ nu (fun x ⇒ appr F ((fun x ⇒ C2 y x) x)))); auto with sc.
      apply sc_nu with L; intros.
      apply sc_F_nuC_nuFC. apply cnew_rename with x; auto.
      apply sc_trans with (nu (fun y ⇒ (nu (fun x ⇒ appr F (C2 x y))))); auto with sc.
      apply sc_nu with L; intros. apply sc_symmetric.
      apply sc_F_nuC_nuFC. change (conc_new
          ((fun a0 ⇒ fun x0 ⇒ C2 x0 a0) a0) (C''0 a0)).
      apply cnew_rename with y; auto.
        intros_all. constructor. intros. forwards*: H14 b0.
        simpl_notin.
  + splits; introv Hlts; intros; simpl_lts.
  + splits; introv Hlts; intros; simpl_lts.
  +
    splits; introv Hlts; intros;
    simpl_lts; forwards*: IHHstruct1 (mapV f P);
    forwards*: IHHstruct2 (mapV f P');
    forwards_test (@struct_congr Empty_set).
    ×
      eexists; split; eauto with hopi; eauto with sc.
    ×
      eexists; split; eauto with hopi; eauto with sc.
    ×
      assert (conc_wf C'0) by (eapply lts_conc_wf; eauto).
      clears P. forwards_test (@struct_congr Empty_set).
      eexists; split; eauto with hopi; eauto with sc.
    ×
      assert (conc_wf C'0) by (eapply lts_conc_wf; eauto).
      clears P'. forwards_test (@struct_congr Empty_set).
      eexists; split; eauto with hopi; eauto with sc.
    ×
      eexists; split; eauto with hopi.
      apply sc_trans with ((appr F0 C) // mapV f P'); eauto with sc.
    ×
      eexists; split; eauto with hopi.
      apply sc_trans with ((appr F0 C) // mapV f P); eauto with sc.
    ×
      eexists; split; eauto with hopi.
      apply sc_trans with ((appr F C0) // mapV f P'); eauto with sc.
    ×
      eexists; split; eauto with hopi.
      apply sc_trans with ((appr F C0) // mapV f P); eauto with sc.
  +
    splits; introv Hlts; intros;
    simpl_lts; eexists; split; eauto with hopi;
    try solve [ind_conc; simpl; auto_sc_nu].
  +
    splits; introv Hlts; intros;
    simpl_lts; eexists; split; eauto with hopi.
    simpl. apply sc_par; auto with sc.
    apply sc_bind; auto with sc.
    intros [|]; simpl; auto with sc.
  +
    splits; introv Hlts; intros; simpl_lts.
    × fresh_lp (L0++L) ((mapV f (nu P)) // (nu P') // mapV f (nu Q)).
      forwards*: H2 x. forwards*: H0 x f.
      forwards_test (@struct_congr Empty_set).
      exp x Q'0. ∃ (nu Q'1); split.
      apply ltsp_new with L0; intros.
      change (ltsproc ((fun x ⇒ mapV f (Q x)) a) (Q'1 a)).
      eapply ltsproc_rename with x; eauto with hopi.
      apply sc_nu with L; intros.
      apply sc_rename with x; auto with hopi.
    × fresh_lpc (a::(L0++L)) (shiftV (mapV f (nu P)) // (nu F0) // shiftV (mapV f (nu Q))) C.
      assert (∀ z, z ≠ x → notin x (mapV f (Q z))) by eauto with hopi.
      assert (∀ z, z ≠ x → notin x (mapV f (P z))) by eauto with hopi.
      clear H8 H10. forwards*: H3 x. auto with hopi. forwards*: H0 x f.
      forwards_test (@struct_congr Empty_set).
      exp x F'0. ∃ (nu F'1); split.
      apply ltsa_new with L0; intros.
      change (ltsabs ((fun x ⇒ mapV f (Q x)) b) a (F'1 b)).
      apply ltsabs_rename with a x; eauto with hopi.
        intros_all. forwards*: H4 b0.
      apply sc_trans with (nu (fun x ⇒ appr (F0 x) C)); auto with sc.
      apply sc_trans with (nu (fun x ⇒ appr (F'1 x) C)); auto with sc.
      apply sc_nu with L; intros.
      change (struct_congr ((fun a0 ⇒ appr (F0 a0) C) a0)
        ((fun a0 ⇒ (appr (F'1 a0) C)) a0)).
      apply sc_rename with x; auto with hopi.
    × fresh_lpc (a::(L0++L)) (shiftV (mapV f (nu P)) // F // shiftV (mapV f (nu Q)))(conc_nu C0).
      assert (∀ z, z ≠ x → notin x (mapV f (Q z))) by eauto with hopi.
      assert (∀ z, z ≠ x → notin x (mapV f (P z))) by eauto with hopi.
      clear H8 H7. forwards*: H2 x. auto with hopi. forwards*: H0 x f.
      forwards_test (@struct_congr Empty_set).
      conc_exp x C'0. destruct (exists_cnew C'1) as [C''].
      ∃ C''; split.
      apply ltsc_new with C'1 L0; intros; auto.
      change (ltsconc ((fun x ⇒ mapV f (Q x)) b) a (C'1 b)).
      apply ltsconc_rename with a x; eauto with hopi.
        intros_all. forwards*: H4 b0.
      apply sc_trans with (nu (fun x ⇒ appr F (C'1 x))); auto with sc.
      apply sc_trans with (nu (fun x ⇒ appr F (C0 x))); auto with sc.
      apply sc_nu with L; intros.
      change (struct_congr ((fun a0 ⇒ appr F (C0 a0)) a0)
        ((fun a0 ⇒ (appr F (C'1 a0))) a0)).
      apply sc_rename with x; auto with hopi.
  +
    splits; introv Hlts; intros;
    forwards*: IHHstruct1 (mapV f P);
    forwards*: IHHstruct2 (mapV f Q);
    do 2 forwards_test (@struct_congr Empty_set); eexists;
      split; try eassumption; eauto with sc.
Qed.

Notation sc0 := (@struct_congr Empty_set).

Lemma struct_congr_sim: simulation sc0.
Proof.
  intros P Q Hstruct.
  replace Q with (mapV (fun x ⇒ x) Q) by (apply mapV_id).
  replace P with (mapV (fun x ⇒ x) P) by (apply mapV_id).
  intros; forwards: @struct_congr_sim'; eauto.
Qed.

Lemma struct_congr_bisim: bisimulation sc0.
Proof.
  apply sim_sym_imply_bisim; auto with sc.
  apply struct_congr_sim.
  unfold sym; apply sc_symmetric.
Qed.

Lemma oe_sc0 : ∀ Rel, Rincl sc0 Rel → Rincl sc0 (open_extension Rel).
Proof.
  intros_all. apply× oe_proc0.
Qed.