Library HOC11TransLemmas

Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.
Require Import HOC06FreshLemmas.
Require Import HOC07SizeLemmas.
Require Import HOC08SubstLemmas.
Require Import HOC09GVLemmas.
Require Import HOC10CongrLemmas.




Lemma wfp_agent_in : ∀ a p ap,
  {{p -- LabIn a ->> ap}} → ∃ f, ap = AA f.
Proof.
  introv Ht. inductions Ht.
    eexists. reflexivity.
    elim IHHt.
      introv Hf1. rewrite Hf1. eexists. reflexivity.
    elim IHHt.
      introv Hf1. rewrite Hf1. eexists. reflexivity.
Qed.

Lemma wfp_agent_out : ∀ a p p´´ ap,
  {{p -- LabOut a p´´->> ap}} → ∃ (p´ : wfprocess), ap = AP p´.
Proof.
  introv Ht. inductions Ht.
    eexists. reflexivity.
    elim IHHt.
      introv Hf1. rewrite Hf1. ∃¬ (wfp_Par x q).
    elim IHHt.
      introv Hf1. rewrite Hf1. ∃¬ (wfp_Par p x).
Qed.

Lemma wfp_agent_rem : ∀ X p ap,
  {{p -- LabRem X ->> ap}} → ∃ (p´ : wfprocess), ap = AP p´.
Proof.
  introv Ht. inductions Ht.
    eexists; reflexivity.
    destruct¬ IHHt as (p´ & Heq). ∃ (wfp_Par p´ q). rewrite¬ Heq.
    destruct¬ IHHt as (q´ & Heq). ∃ (wfp_Par p q´). rewrite¬ Heq.
Qed.

Lemma wfp_agent_tau : ∀ p ap,
  {{p -- Tau ->> ap}} → ∃ (p´ : wfprocess), ap = AP p´.
Proof.
  introv Ht. inductions Ht; try solve [eexists; reflexivity].
    inversion IHHt as (p´ & Hp). ∃ (wfp_Par p´ q). rewrite¬ Hp.
    inversion IHHt as (p´ & Hp). ∃ (wfp_Par p p´). rewrite¬ Hp.
Qed.


Lemma act1_in : ∀ a p1 p2 f1,
  {{p1--LabIn a->>(AA f1)}} → {{wfp_Par p1 p2--LabIn a->>(AA (AbsPar1 f1 p2))}}.
Proof.
  introv Ht. fold (par_ag1 (AA f1) p2). constructor¬.
Qed.

Lemma act2_in : ∀ a p1 p2 f2,
  {{p2--LabIn a->>(AA f2)}} → {{wfp_Par p1 p2--LabIn a->>(AA (AbsPar2 p1 f2))}}.
Proof.
  introv Ht. fold (par_ag2 p1 (AA f2)). constructor¬.
Qed.

Lemma act1_out : ∀ a p1 p1´ p1´´ p2,
  {{p1--LabOut a p1´´->>(AP p1´)}} → {{wfp_Par p1 p2--LabOut a p1´´->>(AP (wfp_Par p1´ p2))}}.
Proof.
  introv Ht. fold (par_ag1 (AP p1´) p2). constructor¬.
Qed.

Lemma act2_out : ∀ a p1 p2 p2´ p2´´,
  {{p2--LabOut a p2´´->>(AP p2´)}} → {{wfp_Par p1 p2--LabOut a p2´´->>(AP (wfp_Par p1 p2´))}}.
Proof.
  introv Ht. fold (par_ag2 p1 (AP p2´)). constructor¬.
Qed.

Lemma act1_rem : ∀ X p1 p1´ p2,
  {{p1--LabRem X->>(AP p1´)}} → {{wfp_Par p1 p2--LabRem X->>(AP (wfp_Par p1´ p2))}}.
Proof.
  introv Ht. fold (par_ag1 (AP p1´) p2). constructor¬.
Qed.

Lemma act2_rem : ∀ X p1 p2 p2´,
  {{p2--LabRem X->>(AP p2´)}} → {{wfp_Par p1 p2--LabRem X->>(AP (wfp_Par p1 p2´))}}.
Proof.
  introv Ht. fold (par_ag2 p1 (AP p2´)). constructor¬.
Qed.

Lemma act1_tau : ∀ p1 p1´ p2,
  {{p1-- Tau ->>(AP p1´)}} → {{wfp_Par p1 p2 -- Tau ->> (AP (wfp_Par p1´ p2))}}.
Proof.
  introv Ht. fold (par_ag1 (AP p1´) p2). constructor¬.
Qed.

Lemma act2_tau : ∀ p1 p2 p2´,
  {{p2-- Tau ->>(AP p2´)}} → {{wfp_Par p1 p2-- Tau ->>(AP (wfp_Par p1 p2´))}}.
Proof.
  introv Ht. fold (par_ag2 p1 (AP p2´)). constructor¬.
Qed.

Ltac solve_transitions :=
  try applys× act1_in; try applys× act2_in;
  try applys× act1_out; try applys× act2_out;
  try applys× act1_rem; try applys× act2_rem;
  try applys× act1_tau; try applys× act2_tau.

Ltac automate :=
  repeat subst_wfp;
  repeat rewrite_wfp_subst;
  repeat rewrite_wfp_swap;
  repeat rewrite_wfp_swap_chan;
  repeat rewrite_wfp_prod;
  repeat rewrite_wfp_pipe_multi;
  try solve_wfp_size;
  try solve_wfp_sizeP;
  try solve [repeat solve_transitions; jauto].


Lemma trans_GV : ∀ (p : wfprocess) X,
  (X \in (GV p)) → (∃ (p´ : wfprocess), {{p -- LabRem X ->> (AP p´)}})
    ∨ (∃ a, ∃ f, {{p -- LabIn a ->> (AA f)}})
    ∨ (∃ a, ∃ (p´ : wfprocess), ∃ p´´, {{p -- LabOut a p´´ ->> (AP p´)}}).
Proof with automate.
  induction p using (measure_induction wfp_size).
  lets Hcp : wf_characterize p; introv Hgv.
  destruct Hcp as [[a [p´ Heq]] | [[a [X´ [p´ Heq]]] | [[X´ Heq] | [[p1 [p2 Heq]] | ]]]]; subst; simpls.
    branch 3. repeat eexists; auto.
    branch 2. repeat eexists; auto.
    rewrite in_singleton in Hgv; subst.
    branch 1. repeat eexists; auto.
    rewrite in_union in Hgv; inverts Hgv as Hgv; specializes H Hgv...
    destruct H as [[p´ Ht] | [[a [f Ht]] | [a [p´ [p´´ Ht]]]]].
      branch 1. ∃ (wfp_Par p´ p2)...
      branch 2. ∃ a (AbsPar1 f p2)...
      branch 3. ∃ a (wfp_Par p´ p2) p´´...
   destruct H as [[p´ Ht] | [[a [f Ht]] | [a [p´ [p´´ Ht]]]]].
      branch 1. ∃ (wfp_Par p1 p´)...
      branch 2. ∃ a (AbsPar2 p1 f)...
      branch 3. ∃ a (wfp_Par p1 p´) p´´...

    rewrite× in_empty in Hgv.
Qed.

Lemma trans_CHS : ∀ (p : wfprocess),
  (CHS p) ≠ \{} → (∃ a, ∃ f, {{p -- LabIn a ->> (AA f)}})
    ∨ (∃ a, ∃ (p´ : wfprocess), ∃ p´´, {{p--LabOut a p´´->>(AP p´)}}).
Proof with automate.
  induction p using (measure_induction wfp_size).
  lets Hcp : wf_characterize p; introv Hgv.
  destruct Hcp as [[a [p´ Heq]] | [[a [X´ [p´ Heq]]] | [[X´ Heq] | [[p1 [p2 Heq]] | ]]]]; subst; simpls; try solve [false¬ Hgv].
      right. repeat eexists; auto.
      left; repeat eexists; auto.
      apply union_not_empty in Hgv. destruct Hgv; specializes H H0...
        destruct H.
          destruct H as (a & f & Ht). left. ∃ a (AbsPar1 f p2)...
          destruct H as (a & p´ & p´´ & Ht). right. ∃ a (wfp_Par p´ p2) p´´...
       destruct H.
          destruct H as (a & f & Ht). left. ∃ a (AbsPar2 p1 f)...
          destruct H as (a & p´ & p´´ & Ht). right. ∃ a (wfp_Par p1 p´) p´´...
Qed.


Lemma false_trans_in: ∀ a (p : wfprocess) fp, a ### p → ¬{{p--LabIn a->>fp}}.
Proof.
  introv Hf Ht; inductions Ht; try solve [simpls; rewrite× cfresh_par_iff in Hf].
    rewrite wfp_cfresh_Abs in Hf. false¬ Hf.
Qed.

Lemma false_trans_out : ∀ a (p : wfprocess) p´ p´´, a ### p → ¬{{p -- LabOut a p´´ ->> p´}}.
Proof.
  introv Hf Ht; inductions Ht; simpls; try solve [rewrite× cfresh_par_iff in Hf].
  rewrite cfresh_send in Hf; false¬ Hf.
Qed.

Lemma false_trans_rem: ∀ X (p : wfprocess) p´, X#p → ¬{{p--LabRem X->>AP p´}}.
Proof.
  introv Hf Ht; inductions Ht; simpls.
    rewrite gfresh_gvar in Hf. false¬ Hf.
    destruct ap; inverts x. rewrite× gfresh_par_iff in Hf.
    destruct aq; inverts x. rewrite× gfresh_par_iff in Hf.
Qed.


Lemma wfp_decomposition_tau1 : ∀ p p´,
  {{p -- Tau ->> (AP p´)}} →
    ∃ a, ∃ (p1 : wfprocess), ∃ p´´, ∃ fp,
      {{p -- LabOut a p´´ ->> (AP p1)}} ∧
      {{p1 -- LabIn a ->> (AA fp)}} ∧
      p´ = wfp_inst_Abs fp p´´.
Proof with automate.
  introv Ht; inductions Ht.
    rename p´ into p´´.
    lets (p´ & Hp´) : wfp_agent_tau Ht; subst; inverts x.
    lets (a & p1 & p2 & fp & (Hto & Hti & Heq)) : IHHt p´; auto.
    ∃ a (wfp_Par p1 q) p2 (AbsPar1 fp q).
    splits... simpl; fequals.
    lets (q´ & Hq´) : wfp_agent_tau Ht; subst; inverts x.
    lets (a & q1 & q2 & fq & (Hto & Hti & Heq)) : IHHt q´; auto.
    ∃ a (wfp_Par p q1) q2 (AbsPar2 p fq).
    splits... simpl; fequals.
    ∃ a (wfp_Par p´0 q) p´´ (AbsPar2 p´0 fq).
    splits...
    ∃ a (wfp_Par p q´) q´´ (AbsPar1 fp q´).
    splits...
Qed.

Lemma wfp_decomposition_tau2 : ∀ a p (p1 : wfprocess) p´´ fp,
  {{p -- LabOut a p´´ ->> (AP p1)}} →
  {{p1 -- LabIn a ->> (AA fp)}} →
  {{p -- Tau ->> (AP (wfp_inst_Abs fp p´´))}}.
Proof with automate.
  induction p using (measure_induction wfp_size).
  lets Hcp : wf_characterize p; introv Hto Hti.
  destruct Hcp as [[a´ [p´ Heq]] | [[a´ [X´ [p´ Heq]]] | [[X´ Heq] | [[p1´ [p2´ Heq]] | ]]]]; subst; simpls; try solve [inverts Hto].
    inverts Hto; inverts Hti.
    inverts keep Hto...
      destruct ap; inverts H4; inverts Hti.
        destruct ap; inverts H5; simpls...
        fold (par_ag1 (AP (wfp_inst_Abs a0 p´´)) p2´). constructor.
        eapply H... try eassumption. auto.
        destruct aq; inverts H5...
        eapply TrTau1; eassumption.
      destruct aq; inverts H4; inverts Hti.
        destruct ap; inverts H5...
        eapply TrTau2; eassumption.
        destruct aq; inverts H5; simpls...
        fold (par_ag2 p1´ (AP (wfp_inst_Abs a0 p´´))). constructor.
        eapply H...
Qed.


Lemma wfp_trans_swap_in : ∀ a X Y p ap,
  {{p--LabIn a->>(AA ap)}} → ∃ ap´, {{(wfp_swap X Y p)--LabIn a->>(AA ap´)}}
     ∧ (∀ m, wfp_swap X Y (wfp_inst_Abs ap m) = wfp_inst_Abs ap´ (wfp_swap X Y m)).
Proof with automate.
  introv Ht. inductions Ht; simpl...
    ∃ (AbsPure ({{X, Y}}X0) (wfp_swap X Y p)). split.
      constructor.
      introv. simpl. apply¬ wfp_swap_on_subst.
    destruct ap0; inverts x.
    specialize (IHHt a0 (reflexivity _)).
    inversion IHHt as (ap´ & Hp).
    ∃ (AbsPar1 ap´ (wfp_swap X Y q)).
    split...
      introv. simpl... fequals×.
    destruct aq; inverts x.
    specialize (IHHt a0 (reflexivity _)).
    inversion IHHt as (aq´ & Hq).
    ∃ (AbsPar2 (wfp_swap X Y p) aq´).
    split...
      introv. simpl... fequals×.
Qed.

Lemma wfp_trans_swap_inst_Abs_eq : ∀ p a fp,
  {{p -- LabIn a ->> AA fp}} →
     ∀ X Y, X # p → Y # p →
       wfp_swap X Y (wfp_inst_Abs fp (wfp_Gvar X)) = wfp_inst_Abs fp (wfp_Gvar Y).
Proof with automate.
  introv Ht Hfx Hfy.

  tests : (X = Y). rewrite¬ wfp_swap_equal. rename C into Hneq.
  gen p X Y. inductions fp; introv Ht Hfx Hfy Hneq.

    inverts Ht; [ | destruct ap; inverts H | destruct aq; inverts H].

    rename v into Z; rewrite wfp_gfresh_Abs in ×.
    inverts Hfx; inverts Hfy; simpl.
      rewrite wfp_subst_gvar_idem; rewrite¬ wfp_swap_equal.
      rewrite wfp_subst_gvar_idem.
      rewrite¬ <- wfp_gfresh_subst_is_swap.
      rewrite wfp_subst_gvar_idem.
      rewrite¬ wfp_gfresh_subst_is_swap.
      rewrite¬ wfp_swap_sym.
      rewrite¬ wfp_swap_involutive.
      rewrite <- wfp_gfresh_subst_is_swap.
        rewrite¬ <- wfp_subst_decomposition_g.
        simpl; fresh_solve.

    inverts Ht; [ | destruct aq; inverts H].
    destruct ap; inverts H; rename p0 into p; simpls.
    rewrite gfresh_par_iff in Hfx, Hfy; inverts Hfx; inverts Hfy...
    fequals. apply IHfp with (p := p)...
    rewrite¬ wfp_gfresh_swap_rewrite.

    inverts Ht; [ destruct ap; invert H | ].
    destruct aq; inverts H; simpls.
    rewrite gfresh_par_iff in Hfx, Hfy; inverts Hfx; inverts Hfy...
    fequals. rewrite¬ wfp_gfresh_swap_rewrite.
    apply IHfp with (p := q)...
Qed.

Lemma wfp_trans_swap_chan_in : ∀ a m n p ap,
  {{p--LabIn a->>(AA ap)}} → ∃ ap´, {{(wfp_swap_chan m n p)--LabIn ({{|m,n|}}a)->>(AA ap´)}}
     ∧ (∀ r, wfp_swap_chan m n (wfp_inst_Abs ap r) = wfp_inst_Abs ap´ (wfp_swap_chan m n r)).
Proof with automate.
  introv Ht. inductions Ht; simpl...
    ∃ (AbsPure X (wfp_swap_chan m n p)). split...
      introv. simpl. apply wfp_swap_chan_on_subst.
    destruct ap0; inverts x.
    specialize (IHHt a0 (reflexivity _)).
    inversion IHHt as (ap´ & Hp).
    ∃ (AbsPar1 ap´ (wfp_swap_chan m n q)).
    split...
      introv. simpl... fequals×.
    destruct aq; inverts x.
    specialize (IHHt a0 (reflexivity _)).
    inversion IHHt as (aq´ & Hq).
    ∃ (AbsPar2 (wfp_swap_chan m n p) aq´).
    split...
      introv. simpl... fequals×.
Qed.

Lemma wfp_trans_swap_out : ∀ a X Y p p´ p´´,
  {{p--LabOut a p´´->>(AP p´)}} → {{(wfp_swap X Y p)--LabOut a (wfp_swap X Y p´´)->>(AP (wfp_swap X Y p´))}}.
Proof with automate.
  introv Ht. inductions Ht; simpl...
    destruct ap; inverts x...
    destruct aq; inverts x...
Qed.

Lemma wfp_trans_swap_chan_out : ∀ a m n p p´ p´´,
  {{p--LabOut a p´´->>(AP p´)}} → {{wfp_swap_chan m n p--LabOut ({{|m,n|}}a) (wfp_swap_chan m n p´´)->>(AP (wfp_swap_chan m n p´))}}.
Proof with automate.
  introv Ht. inductions Ht...
    destruct ap; inverts x...
    destruct aq; inverts x...
Qed.

Lemma wfp_trans_swap_rem : ∀ X X´ Y p p´,
  {{p--LabRem Y->>(AP p´)}} → {{wfp_swap X X´ p--LabRem({{X,X´}}Y) ->>(AP(wfp_swap X X´ p´) )}}.
Proof with automate.
  introv Ht. inductions Ht...
    repeat cases_if*; subst; unfold swap_gvar; repeat cases_if×.
    destruct ap; inverts x...
    destruct aq; inverts x...
Qed.

Lemma wfp_trans_swap_chan_rem : ∀ m n X p p´,
  {{p--LabRem X->>(AP p´)}} → {{(wfp_swap_chan m n p)--LabRem X ->>(AP(wfp_swap_chan m n p´))}}.
Proof with automate.
  introv Ht; inductions Ht...
    destruct ap; inverts x...
    destruct aq; inverts x...
Qed.

Lemma wfp_trans_swap_tau : ∀ X Y p p´,
  {{p--Tau->>(AP p´)}} → {{(wfp_swap X Y p)--Tau->>(AP (wfp_swap X Y p´))}}.
Proof.
  introv Ht.
    apply wfp_decomposition_tau1 in Ht.
    destruct Ht as (a & p1 & p´´ & fp & Htout & Htin & Hp).
    apply (wfp_trans_swap_out a X Y) in Htout.
    apply (wfp_trans_swap_in a X Y) in Htin.
    destruct Htin as (ap´ & Htin & Hr).
    lets Ht : wfp_decomposition_tau2 Htin. eassumption.
    rewrite <- Hr in Ht. rewrite¬ <- Hp in Ht.
Qed.

Lemma wfp_trans_swap_chan_tau : ∀ m n (p p´ : wfprocess),
  {{p--Tau->>(AP p´)}} → {{(wfp_swap_chan m n p)--Tau->>(AP (wfp_swap_chan m n p´))}}.
Proof.
  introv Ht.
    apply wfp_decomposition_tau1 in Ht.
    destruct Ht as (a & p1 & p´´ & fp & Htout & Htin & Hp).
    apply (wfp_trans_swap_chan_out a m n) in Htout.
    apply (wfp_trans_swap_chan_in a m n) in Htin.
    destruct Htin as (ap´ & Htin & Hr).
    lets Ht : wfp_decomposition_tau2 Htin. eassumption.
    rewrite <- Hr in Ht. rewrite¬ <- Hp in Ht.
Qed.


Lemma wfp_trans_subst_in : ∀ a X p fp r,
  {{p--LabIn a->>AA fp}} → ∃ fp´, {{wfp_subst r X p--LabIn a->>AA fp´}}
  ∧ ∀ Y, X≠Y → wfp_inst_Abs fp´ (wfp_Gvar Y) = wfp_subst r X (wfp_inst_Abs fp (wfp_Gvar Y)).
Proof with automate.
  introv Ht; inductions Ht...
    tests : (X = X0).
      replace (wfp_subst r X0 (wfp_Abs a X0 p)) with (wfp_Abs a X0 p).
      ∃ (AbsPure X0 p); split...
        introv Hneq; simpl. rewrite (wfp_gfresh_subst_rewrite _ _ r); auto; try fresh_solve.
      simpl; fresh_solve.
      rewrite¬ wfp_eq_subst_abs1.

    lets H : wfp_eq_subst_abs3 r a p C.
    lets (Z & Hfz) : find_fresh (proc p :: proc r :: Gvar X :: nil);
      rewrite Forall_to_conj_3 in Hfz; destruct Hfz as (Hfzp & Hfzr & Hfzx); rewrite gfresh_gvar in Hfzx.
    specializes¬ H Hfzp; rewrite H;
      eexists. split. constructor.
      introv Hneq. simpl.
      rewrite¬ wfp_substs_commute_gg; simpl; fresh_solve.
      rewrite¬ <- wfp_subst_decomposition_g.
    destruct ap; inverts x...
    specialize (IHHt a0 (reflexivity _)).
    destruct IHHt as (fp´ & Ht´ & Heq).
    ∃ (AbsPar1 fp´ (wfp_subst r X q)). split...
      introv Hneq. simpl... fequals¬.
    destruct aq; inverts x...
    specialize (IHHt a0 (reflexivity _)).
    destruct IHHt as (fq´ & Ht´ & Heq).
    ∃ (AbsPar2 (wfp_subst r X p) fq´). split...
      introv Hneq. simpl... fequals¬.
Qed.

Lemma wfp_trans_Msubst_in :
  ∀ (a : chan) (xs : list var) (rs : list wfprocess)
         (p : wfprocess) (fp : abstraction),
    {{p -- LabIn a ->> AA fp}} →
    length xs = length rs →
    ∃ (fp´ : abstraction),
      ∃ (H´ : {{(wfp_multisubst (combine xs rs) p) -- LabIn a ->> AA fp´}}),
        ∀ Y, ¬Mem Y xs →
          wfp_inst_Abs fp´ (wfp_Gvar Y) =
          wfp_multisubst (combine xs rs) (wfp_inst_Abs fp (wfp_Gvar Y)).
Proof.
  induction xs; introv Ht Hls.
    simpls. ∃ fp Ht. split¬.

    lets Hls´: Hls.
    rewrite length_cons in Hls´. symmetry in Hls´. apply lengthn in Hls´.
    destruct Hls´ as (r & rs´ & Hys). subst.
    asserts Hls´: (length xs = length rs´).
      rewrite_all length_cons in Hls. nat_math.
    destruct¬ (IHxs rs´ p fp Ht) as (fp´ & Ht´ & H´).
    apply (wfp_trans_subst_in a a0 (wfp_multisubst (combine xs rs´) p) fp´ r) in Ht´.
    destruct Ht´ as (fp´´ & Ht´´ & H´´). ∃ fp´´. split; auto.
      simpls¬.
      introv Hm. rewrite Mem_cons_eq in Hm. rew_logic in Hm. destruct Hm. rewrite¬ H´´.
      repeat rewrite_wfp_subst. rewrite¬ <- H´.
Qed.

Lemma wfp_trans_subst_name_in:
  ∀ (a m : chan) (X : var) (p : wfprocess) (fp1 : abstraction),
  {{wfp_subst (wfp_Send m wfp_Nil) X p -- LabIn a ->> AA fp1}} →
  ∃ fp, ∃ (H´ : {{p--LabIn a->>AA fp}}), ∀ Y, X≠Y →
    wfp_inst_Abs fp1 (wfp_Gvar Y) = wfp_subst (wfp_Send m wfp_Nil) X (wfp_inst_Abs fp (wfp_Gvar Y)).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; repeat rewrite_wfp_subst; introv Ht; try solve [try cases_if; inverts Ht].

  tests : (X0 = X).
  replace (wfp_subst (wfp_Send m wfp_Nil) X (wfp_Abs a0 X p0)) with (wfp_Abs a0 X p0) in Ht.
  eexists. ∃ Ht; introv Hneq.
    rewrite¬ wfp_gfresh_subst_rewrite.
    eapply wfp_fresh_inst_Abs; auto; try eassumption.
    rewrite¬ wfp_gfresh_Abs.
    rewrite¬ wfp_eq_subst_abs1.

    rewrite¬ wfp_eq_subst_abs2 in Ht; fresh_solve.
    lets Heq : wfp_trans_in_chan_eq Ht; subst.
    lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; subst.
    eexists. constructor¬.
    introv Hneq; simpl.
    rewrite¬ wfp_substs_commute_gg; simpls; fresh_solve.

    destruct Hyp as (Y & Hneq & Hf & Heq); subst.
    eexists. constructor¬.
    introv Hneq1; simpls.
    rewrite¬ <- wfp_subst_decomposition_g.
    rewrite¬ wfp_substs_commute_gg; simpls. rewrite¬ gfresh_gvar.
    rewrite gfresh_send; apply gfresh_nil.

    inverts Ht...
    destruct ap; inverts H4; rename a0 into fp.
    apply H in H3...
    destruct H3 as (fp´ & Ht´ & Hsub).
    ∃ (AbsPar1 fp´ p2). split...
    introv Hneq; simpls... fequals×.

    destruct aq; inverts H4; rename a0 into fp.
    apply H in H3...
    destruct H3 as (fp´ & Ht´ & Hsub).
    ∃ (AbsPar2 p1 fp´). split...
    introv Hneq; simpls... fequals×.
Qed.

Lemma wfp_trans_Msubst_name_in:
  ∀ (a : chan) (xs : list var) (ms : list chan)
         (p : wfprocess) (fp1 : abstraction),
    {{wfp_multisubst (combine xs (¬¬ms)) p -- LabIn a ->> AA fp1}} →
    length xs = length ms →
      ∃ (fp : abstraction), ∃ (H´ : {{p -- LabIn a ->> AA fp}}),
        ∀ Y, ¬Mem Y xs →
          wfp_inst_Abs fp1 (wfp_Gvar Y) =
          wfp_multisubst (combine xs (¬¬ms)) (wfp_inst_Abs fp (wfp_Gvar Y)).
Proof.
  induction xs; introv Ht Hls.
    simpls.
    ∃× fp1 Ht.

    lets Hls´: Hls.
    rewrite length_cons in Hls´. symmetry in Hls´. apply lengthn in Hls´.
    destruct Hls´ as (m & ms´ & Hys). subst.
    asserts Hls´: (length xs = length ms´).
      rewrite_all length_cons in Hls. nat_math.
    simpls. lets Ht´ : Ht.
    apply wfp_trans_subst_name_in in Ht. destruct Ht as (fp & Ht & Hsub).
    destruct¬ (IHxs ms´ p fp Ht) as (fp´ & Ht´´ & H´).
    ∃ fp´ Ht´´.
    introv Hnm. rewrite Mem_cons_eq in Hnm. rew_logic in Hnm. destruct Hnm.
      specializes H´ Y H0. specializes Hsub Y.
    rewrite H´ in Hsub. applys¬ Hsub.
Qed.

Lemma wfp_trans_subst_name_out : ∀ a m X (p p1´ p1´´ : wfprocess), a ≠ m →
  {{wfp_subst (wfp_Send m wfp_Nil) X p -- LabOut a p1´´ ->> AP p1´}} → ∃ (p´ p´´ : wfprocess),
  {{p--LabOut a p´´->>AP p´}} ∧ p1´ = wfp_subst (wfp_Send m wfp_Nil) X p´ ∧ p1´´ = (wfp_subst (wfp_Send m wfp_Nil) X p´´).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; repeat rewrite_wfp_subst; introv Hf Ht; try solve [inverts¬ Ht].

  inverts Ht...
  eexists; eexists; splits; [constructor | | ]...
  cases_if; inverts Ht...

  inverts Ht...
    destruct ap; inverts H4.
      specializes¬ H H3...
      destruct H as (p´ & p´´ & Ht & Hr1 & Hr2).
      ∃ (wfp_Par p´ p2) p´´... splits...
        rewrite¬ <- Hr1.
    destruct aq; inverts H4.
      specializes¬ H H3...
      destruct H as (p´ & p´´ & Ht & Hr1 & Hr2).
      ∃ (wfp_Par p1 p´) p´´... splits...
        rewrite¬ <- Hr1.
Qed.

Lemma wfp_trans_Msubst_name_out :
  ∀ (a : chan) (xs : list var) (ms : list chan) (p p1´ p1´´ : wfprocess),
    length xs = length ms →
    ¬Mem a ms →
    {{wfp_multisubst (combine xs (¬¬ms)) p -- LabOut a p1´´ ->> AP p1´}} →
      ∃ (p´ p´´ : wfprocess),
        {{p -- LabOut a p´´ ->> AP p´}} ∧
         p1´ = (wfp_multisubst (combine xs (¬¬ms)) p´) ∧
         p1´´ = (wfp_multisubst (combine xs (¬¬ms)) p´´).
Proof.
  induction xs; introv Hls Hm Ht.
    rewrite length_nil in Hls. symmetry in Hls. apply length0 in Hls. subst. simpls.
    ∃¬ p1´ p1´´.
    lets Hls´: Hls. rewrite length_cons in Hls´. symmetry in Hls´.
    apply lengthn in Hls´. destruct Hls´ as (m & ms´ & Hys). subst.
    simpl. rewrite_all length_cons in Hls. simpl in Ht. rewrite Mem_cons_eq in Hm.
    rew_logic in Hm. destruct Hm as (Hneq & Hm).
    apply wfp_trans_subst_name_out in Ht; auto.
    destruct Ht as (p´ & p´´ & Ht & Hr1 & Hr2).
    specializes¬ IHxs Ht. destruct IHxs as (p´0 & p´´0 & Ht´ & Hr1´ & Hr2´).
    ∃ p´0 p´´0. splits¬.
      rewrite¬ <- Hr1´.
      rewrite¬ <- Hr2´.
Qed.

Lemma wfp_trans_subst_out : ∀ a X p p´ p´´ q,
  {{p--LabOut a p´´->>AP p´}} → {{wfp_subst q X p--LabOut a (wfp_subst q X p´´)->>AP (wfp_subst q X p´)}}.
Proof with automate.
  introv Ht; inductions Ht...
    destruct ap; inverts x...
    destruct aq; inverts x...
Qed.

Lemma wfp_trans_Msubst_out : ∀ (a : chan) (p p´ p´´ : wfprocess),
  {{p -- LabOut a p´´ ->> (AP p´)}} →
    ∀ (xs : list var) (ms : list chan), length xs = length ms →
      {{wfp_multisubst (combine xs (¬¬ms)) p
         --LabOut a (wfp_multisubst (combine xs (¬¬ms)) p´´)->>
         AP (wfp_multisubst (combine xs (¬¬ms)) p´)}}.
Proof.
  induction xs.
    simpls¬.
    introv Hls. lets Hls´: Hls. rewrite length_cons in Hls´.
     symmetry in Hls´. apply lengthn in Hls´. destruct Hls´ as (Y & YS´ & HYS).
     subst. simpls. applys¬ wfp_trans_subst_out.
Qed.

Lemma wfp_trans_subst_rem : ∀ X Y p p´ r,
  X ≠ Y → {{p--LabRem X->>AP p´}} → {{(wfp_subst r Y p)--LabRem X->>(AP (wfp_subst r Y p´))}}.
Proof with automate.
  introv Hneq Ht. inductions Ht...
    cases_if...
    destruct ap; inverts x...
    destruct aq; inverts x...
Qed.


Lemma wfp_inst_subst : ∀ fp a X (p : wfprocess) m,
  {{p -- LabIn a ->> AA fp}} → X#p → wfp_inst_Abs fp m = wfp_subst m X (wfp_inst_Abs fp (wfp_Gvar X)).
Proof with automate.
  inductions fp; introv Ht; inverts Ht;
    try solve [destruct ap; inverts H];
    try solve [destruct aq; inverts H]; introv Hf; simpl.

  rewrite wfp_gfresh_Abs in Hf; inverts Hf.
    rewrite¬ wfp_subst_gvar_idem.
    rewrite¬ <- wfp_subst_decomposition_g; fresh_solve.

  destruct ap; inverts H.
  simpls; rewrite gfresh_par_iff in Hf; inverts Hf as (Hf1 & Hf2).
  specializes IHfp m H0; try eassumption...
  rewrite IHfp; fequals×.
  rewrite¬ wfp_gfresh_subst_rewrite.

  destruct aq; inverts H.
  simpls; rewrite gfresh_par_iff in Hf; inverts Hf as (Hf1 & Hf2).
  specializes IHfp m H1; try eassumption...
  rewrite IHfp; fequals×.
  rewrite¬ wfp_gfresh_subst_rewrite.
Qed.

Lemma wfp_inst_swap : ∀ a X Y (p : wfprocess) m fp,
  X#p → Y#p → {{p--LabIn a->>(AA fp)}} → wfp_swap X Y (wfp_inst_Abs fp m) = wfp_inst_Abs fp (wfp_swap X Y m).
Proof with (try solve [fresh_solve]; automate).
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Hf1 Hf2 Ht; try solve [inverts Ht].

    rewrite wfp_gfresh_Abs in ×.
    lets Heq : wfp_trans_in_chan_eq Ht; subst.
    lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; subst; simpl.
    inverts Hf1; inverts Hf2.
      repeat rewrite¬ wfp_swap_equal.
      rewrite wfp_swap_on_subst.
      unfold swap_gvar; cases_if×.
      rewrite <- wfp_gfresh_subst_is_swap with (p := p0)...
      rewrite¬ <- wfp_subst_decomposition_g...
      rewrite wfp_swap_on_subst.
      unfold swap_gvar; repeat cases_if*; subst.
      repeat rewrite¬ wfp_swap_equal.
      rewrite (wfp_swap_sym p0).
      rewrite <- wfp_gfresh_subst_is_swap with (p := p0)...
      rewrite¬ <- wfp_subst_decomposition_g...
      rewrite wfp_swap_on_subst.
      unfold swap_gvar; repeat cases_if*; subst.
      rewrite wfp_gfresh_swap_rewrite with (p := p0); auto.
      repeat rewrite¬ wfp_gfresh_subst_rewrite.
      rewrite (wfp_gfresh_subst_rewrite _ p0)...
      rewrite (wfp_gfresh_swap_rewrite _ _ p0)...
      rewrite¬ wfp_gfresh_subst_rewrite.
      rewrite (wfp_gfresh_swap_rewrite _ _ p0)...

    destruct Hyp as (Z & Hneq & Hfz & Heq); subst; simpl.
    repeat rewrite¬ <- wfp_subst_decomposition_g. clear dependent Z.
    inverts Hf1; inverts Hf2.
      repeat rewrite¬ wfp_swap_equal.
      rewrite wfp_swap_on_subst.
      unfold swap_gvar; cases_if×.
      rewrite <- wfp_gfresh_subst_is_swap with (p := p0)...
      rewrite¬ <- wfp_subst_decomposition_g...
      rewrite wfp_swap_on_subst.
      unfold swap_gvar; repeat cases_if*; subst.
      repeat rewrite¬ wfp_swap_equal.
      rewrite (wfp_swap_sym p0).
      rewrite <- wfp_gfresh_subst_is_swap with (p := p0)...
      rewrite¬ <- wfp_subst_decomposition_g...
      rewrite wfp_swap_on_subst.
      unfold swap_gvar; repeat cases_if*; subst.
      rewrite wfp_gfresh_swap_rewrite with (p := p0); auto.
      repeat rewrite¬ wfp_gfresh_subst_rewrite.
      rewrite (wfp_gfresh_subst_rewrite _ p0)...
      rewrite (wfp_gfresh_swap_rewrite _ _ p0)...
      rewrite¬ wfp_gfresh_subst_rewrite.
      rewrite (wfp_gfresh_swap_rewrite _ _ p0)...

  inverts Ht; repeat subst_wfp.
    destruct ap; inverts H4.
    simpls; rewrite gfresh_par_iff in Hf1, Hf2; rewrite_wfp_swap. fequals×.
    eapply H with (y := p1); jauto...
    rewrite× wfp_gfresh_swap_rewrite.
    destruct aq; inverts H4; simpls.
    rewrite gfresh_par_iff in Hf1, Hf2; rewrite_wfp_swap. fequals×.
    rewrite× wfp_gfresh_swap_rewrite.
    eapply H with (y := p2); jauto...
Qed.

Lemma wfp_inst_chan_swap : ∀ a m n (p : wfprocess) q fp,
  m###p → n###p → {{p--LabIn a->>(AA fp)}} → wfp_swap_chan m n (wfp_inst_Abs fp q) = wfp_inst_Abs fp (wfp_swap_chan m n q).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Hfm Hfn Ht; try solve [inverts Ht].
  lets Heq : wfp_trans_in_chan_eq Ht; subst.
  rewrite wfp_cfresh_Abs in ×.
  destruct Hfm as (Hfm & Hneqm); destruct Hfn as (Hfn & Hneqn).
  lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; subst; simpls.
  rewrite wfp_swap_chan_on_subst.
  rewrite wfp_fresh_chan_swap with (p := p0); auto.
  destruct Hyp as (Y & Hneqy & Hfy & Heq); subst; simpls.
  repeat rewrite wfp_swap_chan_on_subst...
  rewrite wfp_fresh_chan_swap with (p := p0); auto.

  inverts Ht...
    destruct ap; inverts H4; simpls; rewrite cfresh_par_iff in Hfm, Hfn...
    fequals×.
    apply H with (y := p1); jauto...
    applys× wfp_fresh_chan_swap.
    destruct aq; inverts H4; simpls; rewrite cfresh_par_iff in Hfm, Hfn...
    fequals×.
    applys× wfp_fresh_chan_swap.
    apply H with (y := p2); jauto...
Qed.

Lemma wfp_swap_fresh_trans_out : ∀ a X Y (p : wfprocess) p´ p´´,
  X#p → Y#p → {{p--LabOut a p´´->> (AP p´)}} → wfp_swap X Y p´ = p´ ∧ wfp_swap X Y p´´ = p´´.
Proof with automate.
  introv Hf1 Hf2 Ht. inductions Ht...
    split¬... simpls; rewrite gfresh_send in Hf1, Hf2. rewrite¬ wfp_gfresh_swap_rewrite.
    destruct ap; inverts x... simpls; rewrite gfresh_par_iff in Hf1, Hf2.
    destruct Hf1 as (Hf11 & Hf12).
    destruct Hf2 as (Hf21 & Hf22).
    forwards¬ (IHHt1 & IHHt2): IHHt w.
    splits~; simpls~; fequals¬.
      rewrite¬ wfp_gfresh_swap_rewrite.
    destruct aq; inverts x... simpls; rewrite gfresh_par_iff in Hf1, Hf2.
    destruct Hf1 as (Hf11 & Hf12). destruct Hf2 as (Hf21 & Hf22).
    forwards¬ (IHHt1 & IHHt2): IHHt w.
    splits~; simpls~; fequals.
      rewrite× wfp_gfresh_swap_rewrite.
Qed.

Lemma wfp_cswap_fresh_trans_out : ∀ a m n (p : wfprocess) p´ p´´,
  m###p → n###p → {{p--LabOut a p´´->> (AP p´)}} → wfp_swap_chan m n p´ = p´ ∧ wfp_swap_chan m n p´´ = p´´.
Proof with (try applys× wfp_fresh_chan_swap; automate).
  introv Hf1 Hf2 Ht. inductions Ht...
    split~; simpls. rewrite cfresh_send in Hf1, Hf2...
    destruct ap; inverts x... simpls; rewrite cfresh_par_iff in Hf1, Hf2.
    destruct Hf1 as (Hf11 & Hf12). destruct Hf2 as (Hf21 & Hf22).
    forwards¬ (IHHt1 & IHHt2): IHHt w.
    splits~; simpls~; fequals...
    destruct aq; inverts x... simpls; rewrite cfresh_par_iff in Hf1, Hf2.
    destruct Hf1 as (Hf11 & Hf12). destruct Hf2 as (Hf21 & Hf22).
    forwards¬ (IHHt1 & IHHt2): IHHt w.
    splits~; simpls~; fequals...
Qed.


Lemma wfp_subst_both: ∀ X p q r, p = q → (wfp_subst r X p) = (wfp_subst r X q).
Proof.
  introv He. rewrite¬ He.
Qed.

Lemma cp_subst_dist: ∀ X p fp (r : wfprocess), closed_process r →
wfp_subst r X (wfp_inst_Abs fp p) = wfp_subst r X (wfp_inst_Abs fp (wfp_subst r X p)).
Proof with (try solve [unfold fresh_gvar; rewrite Hcp; apply notin_empty]).
  introv Hcp. induction fp; simpls; repeat rewrite_wfp_subst; try solve [fequals*].
    unfolds in Hcp.
    tests : (v = X).
      rewrite wfp_gfresh_subst_rewrite with (p := (wfp_subst (wfp_subst r X p) X w)); repeat (simpls; fresh_solve); auto...
      rewrite¬ wfp_subst_on_subst_same...
      rewrite¬ wfp_subst_on_subst... rewrite¬ wfp_substs_commute_gg; simpl; fresh_solve...
Qed.

Lemma wfp_trans_subst_tau: ∀ X (p p´ r : wfprocess),
  {{p--Tau->>AP p´}} → closed_process r → {{wfp_subst r X p -- Tau ->> (AP (wfp_subst r X p´))}}.
Proof with (try (simpls; fresh_solve; applys¬ wfp_fresh_cp)).
  introv Ht Hcp. apply wfp_decomposition_tau1 in Ht.
  destruct Ht as (a & p1 & p´´ & fp & Hout & Hin & Hp´).
  apply (wfp_trans_subst_out a X p p1 p´´ r) in Hout.
  lets Hin´: Hin.
  apply (wfp_trans_subst_in a X p1 fp r) in Hin; try apply wf_cond; auto.
  destruct Hin as (fp´ & Hin & Hfp).
  lets Htau: wfp_decomposition_tau2 Hout Hin. rewrite Hp´.
  lets (Y & Hf): find_fresh ((Gvar X):: proc p1::nil).
  rewrite Forall_to_conj_2 in Hf. destruct Hf as (Hneq & Hf).
  unfolds in Hneq. simpl in Hneq. rewrite notin_singleton in Hneq.
  apply neq_sym in Hneq. specializes Hfp Y Hneq.
  apply (wfp_subst_both Y _ _ (wfp_subst r X p´´)) in Hfp.
  erewrite <- wfp_inst_subst in Hfp; eauto...
  rewrite¬ wfp_substs_commute_gg in Hfp...
  erewrite <- wfp_inst_subst in Hfp; eauto.
  rewrite¬ <- cp_subst_dist in Hfp. rewrite¬ <- Hfp.
Qed.

Lemma wfp_trans_Msubst_tau: ∀ XS (rs : list wfprocess) (p p´ : wfprocess),
  {{p -- Tau ->> AP p´}} → length XS = length rs →
  closed_proc_list_wfp rs →
  {{wfp_multisubst (combine XS rs) p -- Tau ->> (AP (wfp_multisubst (combine XS rs) p´))}}.
Proof.
  induction XS; introv Ht Hls Hcp.
    simpls¬.
    lets Hls´: Hls.
    rewrite length_cons in Hls´. symmetry in Hls´. apply lengthn in Hls´.
    destruct Hls´ as (r & rs´ & Hys). subst.
    asserts Hls´: (length XS = length rs´).
      rewrite_all length_cons in Hls. nat_math.
    simpls. applys× wfp_trans_subst_tau.
Qed.

Lemma wfp_trans_out_ex_subst : ∀ p a m X p1´ p1´´,
  {{wfp_subst (wfp_Send m wfp_Nil) X p--LabOut a p1´´->>AP p1´}} → ∃ (p´ p´´ : wfprocess),
  p1´ = (wfp_subst (wfp_Send m wfp_Nil) X p´) ∧ p1´´ = (wfp_subst (wfp_Send m wfp_Nil) X p´´)
  ∧ (m###p → m###p´ ∧ m###p´´).
Proof with (freshen_up; automate).
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Ht; repeat rewrite_wfp_subst; inverts Ht;
    try solve [cases_if; inverts H1]...
    ∃ wfp_Nil p0. splits¬...
      introv H1. simpls; rewrite cfresh_send in H1.
      splits×...
    cases_if; inverts H1; subst...
    ∃ wfp_Nil wfp_Nil; repeat rewrite_wfp_subst; splits¬...

    destruct ap; inverts H4.
    specializes H H3...
    destruct H as (p´ & p´´ & Hr1 & Hr2 & Hf); subst.
    ∃ (wfp_Par p´ p2). eexists. splits×...
    introv H; simpls; rewrite cfresh_par_iff in *; splits×.

    destruct aq; inverts H4.
    specializes H H3...
    destruct H as (p´ & p´´ & Hr1 & Hr2 & Hf); subst.
    ∃ (wfp_Par p1 p´). eexists. splits×...
    introv H; simpls; rewrite cfresh_par_iff in *; splits×.
Qed.

Lemma wfp_trans_subst_name_tau: ∀ m X (p ap : wfprocess), m###p →
  {{wfp_subst (wfp_Send m wfp_Nil) X p -- Tau ->> AP ap}} →
  ∃ (p´ : wfprocess), {{p -- Tau ->> AP p´}} ∧ ap = wfp_subst (wfp_Send m wfp_Nil) X p´.
Proof with freshen_up.
  introv Hf Ht. apply wfp_decomposition_tau1 in Ht.
  destruct Ht as (a & p1´ & p1´´ & fp & Htout & Htin & Hap).
  assert (a ≠ m).
    lets (p´ & p´´ & Hp1 & Hp2 & Hfs): (wfp_trans_out_ex_subst p a m X p1´ p1´´ Htout); subst.
    lets (fp0 & Htin´ & Hfa) : (wfp_trans_subst_name_in a m X p´ fp Htin).
    destruct (Hfs Hf) as (Hfmp1 & _).
    introv H1. subst. eapply false_trans_in; eauto.

  apply wfp_trans_subst_name_out in Htout; auto. destruct Htout as (p´ & p´´0 & Htout & Hp1 & Hp2); subst.
  lets (fp0 & Htin´ & Hfa) : (wfp_trans_subst_name_in a m X p´ fp Htin).
  lets H0 : wfp_decomposition_tau2 Htout Htin´.
  ∃ (wfp_inst_Abs fp0 p´´0). split¬.
  lets (Y & HfY): find_fresh ((proc p´)::Gvar X::nil). rewrite Forall_to_conj_2 in HfY.
  destruct HfY as (HfYp1 & Hneq). rewrite gfresh_gvar in Hneq.
  rewrite¬ (wfp_inst_subst fp0 a Y p´ p´´0).
  apply not_eq_sym in Hneq; specialize (Hfa Y Hneq).

  rewrite¬ wfp_subst_on_subst... rewrite¬ <- Hfa.
  rewrite¬ (wfp_inst_subst fp a Y (wfp_subst (wfp_Send m wfp_Nil) X p´) (wfp_subst (wfp_Send m wfp_Nil) X p´´0)).
  simpls; fresh_solve.
Qed.

Lemma wfp_trans_Msubst_name_tau: ∀ XS ms (p : wfprocess) ap,
  length XS = length ms → noDup ms → Forall (fun m ⇒ m###p) ms →
  {{wfp_multisubst (combine XS (¬¬ms)) p--Tau->>AP ap}} → ∃ (p´ : wfprocess), {{p--Tau->>AP p´}} ∧ ap = wfp_multisubst (combine XS (¬¬ms)) p´.
Proof.
  induction XS; introv Hls Hnd Hfs Ht.
    rewrite length_nil in Hls. symmetry in Hls. apply length0 in Hls. subst. simpls×.

    lets Hls´: Hls. rewrite length_cons in Hls. symmetry in Hls. apply lengthn in Hls.
    destruct Hls as (m & ms´ & Hms). subst. simpls.
    rewrite_all length_cons in Hls´. inverts Hfs as Hfm Hfms.
    destruct Hnd as (Hnm & Hnd).
    apply wfp_trans_subst_name_tau in Ht.
    destruct Ht as (p´0 & Ht & Hap). subst. specializes¬ IHXS Ht.
    destruct IHXS as (p´ & Htt & Hp´). subst. ∃ p´. split¬.
    applys¬ wfp_cfresh_Msubst1. clear IHXS Hnd Ht Hls´ Hfms Hfm. induction ms´.
      apply Forall_nil.
      rewrite Mem_cons_eq in Hnm. rew_logic in Hnm. destruct Hnm. applys¬ Forall_cons.
Qed.


Lemma wfp_trans_rem_is_out: ∀ (a : chan) (X : var) (p p´ : wfprocess),
    {{p --LabRem X->> (AP p´)}} →
    {{wfp_subst (wfp_Send a wfp_Nil) X p --LabOut a wfp_Nil->> AP (wfp_subst (wfp_Send a wfp_Nil) X p´)}}.
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Ht; inverts Ht...
    cases_if¬.
    destruct ap; inverts H4...
    apply act1_out. applys¬ H...
    destruct aq; inverts H4...
    apply act2_out; applys¬ H...
Qed.

Lemma wfp_trans_out_is_rem:
  ∀ (a : chan) (X : var) (p p´1 p´´1 : wfprocess),
    a###p → {{wfp_subst (wfp_Send a wfp_Nil) X p --LabOut a p´´1->> AP p´1}} →
      ∃ (p´ : wfprocess),
        {{p --LabRem X->> (AP p´)}} ∧ p´1 = wfp_subst (wfp_Send a wfp_Nil) X p´ ∧ p´´1 = wfp_Nil.
Proof with (try solve [freshen_up]; automate).
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Hf Ht; try solve [try cases_if*; inverts Ht];
  rewrite_wfp_subst; inverts Ht; try cases_if×...

  simpls; false...

  inverts H1...
  ∃ wfp_Nil; splits×...

  destruct ap; inverts H4.
  simpls; rewrite cfresh_par_iff in Hf. destruct Hf as (Hf1 & Hf2).
  specializes H H3...
  destruct H as (p´1 & Ht & Hp1 & Hp2). ∃ (wfp_Par p´1 p2).
    splits... fequals×.

  destruct aq; inverts H4.
  simpls; rewrite cfresh_par_iff in Hf. destruct Hf as (Hf1 & Hf2).
  specializes H H3...
  destruct H as (p´1 & Ht & Hp1 & Hp2). ∃ (wfp_Par p1 p´1).
    splits... fequals×.
Qed.