Require Export Binders TLC.LibEqual TLC.LibRelation TLC.LibTactics.
Require Export TLC.LibNat.

Require Export List.

Parameter name : Set.
Axiom dec_name: ∀ x y:name, x=y ∨ x≠y.

Inductive proc (V : Set) : Set :=
| pr_var : V → proc V
| pr_inp : name → proc (incV V) → proc V
| pr_snd : name → proc V → proc V → proc V
| pr_par : proc V → proc V → proc V
| pr_nu : (name → proc V) → proc V
| pr_nil : proc V
.

Arguments pr_var {V} _.
Arguments pr_inp {V} _ _.
Arguments pr_snd {V} _ _ _.
Arguments pr_par {V} _ _.
Arguments pr_nu {V} _.
Arguments pr_nil {V}.

Notation "a ? P" := (@pr_inp _ a P) (at level 42, right associativity).
Notation "a '!(' P ')' Q" := (@pr_snd _ a P Q) (at level 42, right associativity).
Notation "P '//' Q" := (@pr_par _ P Q) (at level 40, left associativity).
Notation " 'nu' P" := (@pr_nu _ P) (at level 42, right associativity).
Notation PO := (@pr_nil _).

Notation proc0 := (proc Empty_set).
Notation proc1 := (proc (incV Empty_set)).


Inductive isin {V:Set} (x:name) : proc V → Prop :=
| isin_inp : ∀ a P, @isin (incV V) x P → isin x (a ? P)
| isin_inp_name : ∀ P, isin x (x ? P)
| isin_snd1 : ∀ a P Q, isin x P → isin x (a!(P) Q)
| isin_snd2 : ∀ a P Q, isin x Q → isin x (a!(P) Q)
| isin_snd_name : ∀ P Q, isin x (x!(P) Q)
| isin_par1 : ∀ P Q, isin x P → isin x (P // Q)
| isin_par2 : ∀ P Q, isin x Q → isin x (P // Q)
| isin_nu : ∀ P, (∀ z, z≠x → isin x (P z)) → isin x (nu P).

Inductive notin {V:Set} (x:name) : proc V → Prop :=
| notin_var : ∀ v, notin x (pr_var v)
| notin_nil : notin x PO
| notin_inp : ∀ a P, a ≠ x → @notin (incV V) x P → notin x (a ? P)
| notin_snd : ∀ a P Q, a ≠ x → notin x P → notin x Q
                                     → notin x (a!(P) Q)
| notin_par : ∀ P Q, notin x P → notin x Q → notin x (P//Q)
| notin_nu : ∀ P, (∀ z, x≠z → notin x (P z)) → notin x (nu P).

Definition notin_ho {V:Set} a (P:name → proc V) :=
  ∀ b, a≠b → notin a (P b).

Hint Constructors isin notin:hopi.

Ltac head t :=
  match t with
  | ?t' _ ⇒ head t'
  | _ ⇒ t
  end.
Ltac head_constructor t :=
  let t' := head t in is_constructor t'.
Ltac simpl_notin_list :=
  repeat match goal with
  | [ H : ¬ In _ (cons _ _) |- _ ] ⇒
      rewrite not_in_cons in H; destruct H
  | [ H : ¬ In _ (app _ _) |- _ ] ⇒
      rewrite in_app_iff in H; apply Decidable.not_or in H; destruct H
  | [ H : ¬ In _ nil |- _ ] ⇒ clear H
  | [ H : ¬ In _ _ ∧ _ |- _ ] ⇒ destruct H
  | [ |- ¬ In _ (cons _ _) ] ⇒ rewrite not_in_cons; split; auto
  end.
Ltac simpl_notin_proc :=
  repeat match goal with
  | [ H : notin _ ?t |- _ ] ⇒ head_constructor t; inverts H
  | [ H : notin _ _ ∧ _ |- _ ] ⇒ destruct H
  | [ H : _ ∧ notin _ _ |- _ ] ⇒ destruct H
  end.
Ltac simpl_notin :=
  repeat (simpl_notin_list; simpl_notin_proc; simpl in *; auto).

Axiom proc_ext : ∀ {V:Set} x (P Q:name→proc V), notin_ho x P →
  notin_ho x Q → (P x = Q x) → P = Q.

Ltac auto_proc_ext :=
  match goal with
  | [ H : ?P ?X = ?Q ?X |- _ ] ⇒
    (forwards*: @proc_ext X P Q; intros_all; auto with hopi);
    subst; simpl_notin; clear H; auto with hopi
  end.

Axiom beta_exp : ∀ {V:Set} a (P:proc V),
  ∃ P', notin_ho a P' ∧ P = P' a.
Axiom ho_beta_exp : ∀ {V:Set} a (P:name → proc V),
  ∃ P', notin_ho a (fun x ⇒ nu P' x) ∧ P = P' a.
Axiom ho_ho_beta_exp : ∀ {V:Set} a (P:name → name → proc V),
  ∃ P', notin_ho a (fun x ⇒ nu (fun y ⇒ nu P' x y)) ∧ P = P' a.

Ltac exp x P := let Pr := fresh P in
   destruct (beta_exp x P) as [Pr []]; subst.
Ltac ho_exp x P := let Pr := fresh P in
   destruct (ho_beta_exp x P) as [Pr []]; subst.
Ltac ho_ho_exp x P := let Pr := fresh P in
   destruct (ho_ho_beta_exp x P) as [Pr []]; subst.

Ltac all_exp x := repeat match goal with
  | [ P : proc _ |- _ ] ⇒ exp x P
  end.

Ltac change_ext :=
  match goal with
  | [ H : ?Q = ?P ?x |- _ ] ⇒
      let R := (eval pattern x in Q) in change (R = P x) in H; auto_proc_ext
  end.

Ltac exp_ext x := all_exp x; repeat change_ext.

Axiom unsat : ∀ {V:Set} (P:proc V), ∃ a, notin a P.

Ltac fresh_proc P := destruct (unsat P); simpl_notin.

Fixpoint listproc {V:Set} (L : list name) (P : proc V) : proc V :=
  match L with
  | nil ⇒ P
  | cons a L' ⇒ a!(PO)(listproc L' P)
  end.

Lemma listproc_in {V}: ∀ a (P : proc V) L,
    notin a (listproc L P) → ¬In a L ∧ notin a P.
Proof.
  intros.
  induction L; simpl in *; auto.
  simpl_notin.
  forwards*: IHL.
Qed.

Lemma unsat_lp {V}: ∀ L (P : proc V), ∃ a, ¬In a L ∧ notin a P.
Proof.
  intros. fresh_proc (listproc L P).
  ∃ x. forwards*: @listproc_in.
Qed.

Lemma unsat_list: ∀ (L:list name), ∃ a, ¬In a L.
Proof.
  intros. fresh_proc (listproc L (@pr_nil Empty_set)).
  ∃ x. forwards*: @listproc_in.
Qed.

Ltac fresh_lp L P := destruct (unsat_lp L P); simpl_notin.
Ltac fresh_list L := destruct (unsat_list L); simpl_notin.

Lemma sep {V:Set}: ∀ (P:proc V), ∀ a b,
    isin a P → notin b P → a≠b.
Proof.
  induction P; introv Hin Hnotin; inverts Hnotin; inverts Hin; auto.
  fresh_list (a::b::nil). forwards*: H1 x.
Qed.

Lemma isin_not_notin {V:Set}: ∀ (P:proc V),
    ∀ a, isin a P → ¬ notin a P.
Proof.
  intros_all. forwards*: @sep a a.
Qed.

Lemma notin_not_isin {V:Set}: ∀ (P:proc V),
    ∀ a, notin a P → ¬ isin a P.
Proof.
  intros_all. forwards*: @sep a a.
Qed.

Fixpoint mapV {V W: Set} (f : V → W) (P : proc V) : proc W :=
  match P with
  | pr_var x ⇒ pr_var (f x)
  | a ? P ⇒ a ? (mapV (incV_map f) P)
  | a !(P) Q ⇒ a !(mapV f P) (mapV f Q)
  | nu P ⇒ nu (fun x ⇒ mapV f (P x))
  | P // Q ⇒ (mapV f P) // (mapV f Q)
  | PO ⇒ PO
  end.

Notation shiftV := (mapV (@VS _)).
Notation shiftV1 := (mapV (incV_map (@VS _))).

Definition liftV {V W: Set} (f : V → proc W) (x : incV V) :
  proc (incV W) :=
  match x with
  | VZ ⇒ pr_var VZ
  | VS y ⇒ shiftV (f y)
  end.

Fixpoint bind {V W : Set} (f : V → proc W) (P : proc V) : proc W:=
  match P with
  | pr_var x ⇒ f x
  | a ? P ⇒ a ? (bind (liftV f) P)
  | a !(P) Q ⇒ a !(bind f P) (bind f Q)
  | nu P ⇒ nu (fun x ⇒ bind f (P x))
  | P // Q ⇒ (bind f P) // (bind f Q)
  | PO ⇒ PO
  end.

Definition subst_func {V: Set} (P : proc V) (x : incV V) : proc V :=
  match x with
  | VZ ⇒ P
  | VS y ⇒ pr_var y
  end.

Notation subst P Q := (@bind _ _ (@subst_func _ Q) P).

Lemma mapV_id {V: Set} (P : proc V) :
  mapV (fun x ⇒ x) P = P.
Proof.
  induction P; default_simp; auto.
  asserts_rewrite (incV_map (fun (x:V) ⇒ x) = fun x ⇒ x).
   extens. intros [ | x ]; simpl; congruence.
   rewrite× IHP.
  extens; intros. rewrite H. auto.
Qed.

Lemma mapV_mapV {A B C : Set} : ∀ (P : proc A)
  (f : A → B) (g : B → C),
  mapV g (mapV f P) = mapV (fun x ⇒ g (f x)) P.
Proof.
  intros. gen B C. induction P; default_simp.
    rewrite IHP. repeat fequals. extens. intros [ | x]; simpl; try reflexivity.
  extens; intros. rewrite H; auto.
Qed.

Lemma bind_return {V: Set} : ∀ (P : proc V)(f : V → proc V),
  (∀ x, f x = pr_var x) → bind f P = P.
Proof.
  induction P; default_simp.
  + rewrite× IHP. intros [ | x ]; simpl; trivial.
    rewrite× H.
  + extens. intros. rewrite H; simpl; auto.
Qed.

Lemma bind_return' {V: Set} : ∀ (P : proc V), bind (@pr_var _ ) P = P.
Proof.
  intros; apply bind_return; reflexivity.
Qed.

Lemma bind_proc0: ∀ (P: proc0) (f : Empty_set → proc0), bind f P = P.
Proof.
  intros. apply bind_return. intros; inverts x.
Qed.

Lemma bind_mapV {A B1 B2 C : Set} : ∀ (P : proc A )
    (f1 : A → B1) (f2 : B1 → proc C )(g1 : A → proc B2 ) (g2 : B2 → C),
      (∀ x, f2 (f1 x) = mapV g2 (g1 x)) → bind f2 (mapV f1 P) = mapV g2 (bind g1 P).
Proof.
  intros. gen B1 B2 C. induction P; default_simp.
  + erewrite IHP. eauto. intros [ | x ]; simpl; auto.
    rewrite H; repeat rewrite mapV_mapV; reflexivity.
  + extens; intros. erewrite H; eauto.
Qed.

Lemma bind_bind {A B C : Set}: ∀ (P : proc A )(f : A → proc B )
  (g : B → proc C ),
  bind g (bind f P) = bind (fun x ⇒ bind g (f x)) P.
Proof.
  intros. gen B C. induction P; default_simp.
  + rewrite IHP. repeat fequals. extens. intros [ | x ]; simpl; [ reflexivity | ].
    apply bind_mapV; reflexivity.
  + extens; intros. rewrite H. reflexivity.
Qed.

Lemma bind_mapV_comp {A B C :Set}: ∀ P (f:B→proc C )(g:A→B),
  bind f (mapV g P) = bind (fun x ⇒ f (g x)) P.
Proof.
  intros; gen C B. induction P; default_simp.
  + rewrite IHP. fequals. extens. intros [ | x ]; simpl; auto.
  + extens; intros. rewrite H; reflexivity.
Qed.

Lemma subst_shift {V : Set} : ∀ (P Q : proc V ), subst (shiftV P) Q = P.
Proof.
  intros; erewrite bind_mapV.
  + rewrite mapV_id; apply bind_return'.
  + reflexivity.
Qed.


Inductive size {V:Set} : proc V → nat → Prop :=
| sz_var : ∀ v, size (pr_var v) 0
| sz_nil : size (@pr_nil V) 0
| sz_inp : ∀ a P n, @size (incV V) P n → size (a ? P) (1+n)
| sz_out : ∀ a P Q n m, size P n → size Q m → size (a!(P) Q)(1+n+m)
| sz_par : ∀ P Q n m, size P n → size Q m → size (P//Q)(1+n+m)
| sz_nu : ∀ P n, (∀ x, size (P x) n) → size (nu P) (1+n).

Hint Constructors notin isin size:hopi.

Lemma size_rename {V:Set} : ∀ n (P:name→ proc V) x, notin_ho x P →
  size (P x) n → ∀ y, size (P y) n.
Proof with nat_math.
  intros. gen x y V.
  induction n using TLC.LibNat.peano_induction; intros.
  inverts H1; try solve [change_ext].
  + destruct (dec_name a x); subst; exp_ext x;
      constructor; apply H with x; auto...
  + destruct (dec_name a x); subst; exp_ext x;
      constructor; apply H with x; auto...
  + exp_ext x. constructor; apply H with x; auto...
  + ho_exp x P0. change_ext.
    constructor. intros.
    fresh_lp (x::nil) (nu (P1 y)).
    apply H with x1; [nat_math | intros_all; apply H6; auto |].
    change (size ((fun x⇒ P1 x x1) y) n0).
    apply H with x; [nat_math | | apply H3].
    intros_all. forwards*: H1 b. inverts H5. apply H8. auto.
Qed.

Hint Constructors size:hopi.

Lemma exists_sz {V:Set} : ∀ (P:proc V), ∃ n, size P n.
Proof.
  intros; induction P; try solve [eexists; eauto with hopi].
  - destruct IHP. eexists; eauto with hopi.
  - destruct IHP1. destruct IHP2. eexists; eauto with hopi.
  - destruct IHP1. destruct IHP2. eexists; eauto with hopi.
  - fresh_proc (nu p). forwards[n]: H x.
    ∃ (1+n). constructor. intros.
    apply size_rename with x; assumption.
Qed.


Lemma notin_rename' {V:Set}: ∀ n (P:proc V), (size P n) →
      ∀ P' c, (notin_ho c P') → P=(P' c) →
      ∀ a b, (notin a (P' b)) → (notin_ho a P').
Proof with nat_math.
  intro n; gen V.
  induction n using TLC.LibNat.peano_induction;
      introv Hs Hc Hp' Hnotin.
  destruct P; inverts Hs; intros_all; try solve [change_ext].
  - destruct (dec_name n0 c); subst; exp_ext c;
      constructor; auto; apply× H...
  - destruct (dec_name n0 c); subst; exp_ext c;
      constructor; auto.
    1,3:forwards*: H n1 P2...
    all:forwards*: H m P0...
  - exp_ext c. constructor.
    forwards*: H n0 P2...
    forwards*: H m P0...
  - ho_exp c p. rename p0 into P''. change_ext.
    constructor. intros.
    fresh_lp (z::a::c::nil) (nu (P'' b0)). rename x into c'.
    assert (∀ x, x≠c → size (P'' b0 x) n0).
      intros; change (size ((fun c ⇒ P'' c x) b0) n0).
      eapply size_rename; eauto. intros_all.
      forwards*: Hc b1. simpl_notin.
    assert (notin a (P'' b0 c')).
      change (notin a ((fun b0 ⇒ P'' b0 c') b0)).
      eapply H; eauto. nat_math. intros_all.
      forwards*: Hc b1. simpl_notin.
    clear H1. eapply H; eauto...
Qed.

Lemma notin_rename {V:Set}: ∀ (P:name→proc V) a b,
   notin a (P b) → ∀ c, a≠c → notin a (P c).
Proof.
  intros. fresh_proc (nu P).
  destruct (exists_sz (nu P)) as [n]. inverts H1.
  eapply notin_rename'; eauto.
Qed.

Lemma isin_rename' {V:Set}: ∀ n (P:proc V), (size P n) →
      ∀ P' c, (notin_ho c P') → P=(P' c) →
      ∀ a b, a≠b → isin a (P' b) →
      ∀ d, isin a (P' d).
Proof with nat_math.
  intro n; gen V.
  induction n using TLC.LibNat.peano_induction;
      introv Hs Hc Hp' Hab Hin. intros.
  destruct P; inverts Hs; intros_all; try solve [change_ext].
  - destruct (dec_name n0 c); subst; exp_ext c.
    + inverts Hin; [|contradiction].
      constructor. forwards*: H H3...
    + inverts Hin; [|apply isin_inp_name].
      constructor. forwards*: H H4...
  - destruct (dec_name n0 c); subst; exp_ext c.
    + inverts Hin; [| |contradiction].
      × apply isin_snd1. forwards*: H n1 P2 H3...
      × apply isin_snd2. forwards*: H m H3...
    + inverts Hin; [| |apply isin_snd_name].
      × apply isin_snd1. forwards*: H n1 P2 H6...
      × apply isin_snd2. forwards*: H m H6...
  - exp_ext c. inverts Hin.
    + apply isin_par1. forwards*: H n0 P2 H5...
    + apply isin_par2. forwards*: H m H5...
  - ho_exp c p. rename p0 into P''. change_ext.
    inverts Hin. constructor. intros.
    fresh_lp (z::a::c::d::nil) (nu (P'' b)). rename x into c'.
    change (isin a ((fun d ⇒ P'' d z) d)).
    apply H with n0 (P'' c' z) c' b; auto.
    + nat_math.
    +
      fresh_lp (z::a::c::d::nil) (nu (P'' c')). rename x into c''.
      eapply size_rename; eauto.
      change (size ((fun c ⇒ P'' c c'') c') n0).
      eapply size_rename; eauto. intros_all.
      forwards*: Hc b0. simpl_notin.
    +
      intros_all. change (notin c' ((fun b ⇒ P'' b z) b0)).
      eapply notin_rename; eauto.
Qed.

Lemma isin_rename {V:Set}: ∀ (P:name→proc V) a b,
   a≠b → isin a (P b) → ∀ c, isin a (P c).
Proof.
  intros. fresh_proc (nu P).
  destruct (exists_sz (P x)) as [n].
  apply isin_rename' with n (P x) x b; auto.
Qed.

Lemma isin_notin_dec {V:Set}: ∀ a (P:proc V), isin a P ∨ notin a P.
Proof.
  induction P; intuition (auto with hopi).
  - destruct (dec_name a n); subst; intuition (auto with hopi).
  - destruct (dec_name a n); subst; intuition (auto with hopi).
  - fresh_lp (a::nil) (nu p). forwards[]: H x.
    + left. constructor. intros. apply isin_rename with x; eauto.
    + right. constructor. intros. eapply notin_rename; eauto.
Qed.

Lemma isin_arg' {V:Set}: ∀ n (P':proc V), size P' n →
  ∀ P c, notin_ho c P → P' = (P c) →
  ∀ a, notin_ho a P → isin a (P a) →
  ∀ b, isin b (P b).
Proof.
  intros; gen V; induction n using TLC.LibNat.peano_induction; intros.
  inverts H0; auto.
  - change_ext. inverts H4.
  - change_ext. inverts H4.
  - destruct (dec_name a0 c); subst; exp_ext c.
    constructor. eapply H; eauto.
    + nat_math.
    + intros_all. forwards*: H3 b0. simpl_notin.
    + inverts× H4. forwards*: H3 c. inverts× H4.
  - destruct (dec_name a0 c); subst; exp_ext c.
    inverts H4.
    + apply× @isin_snd1. forwards*: H n0 P1. nat_math.
      intros_all. forwards*: H3 b0. simpl_notin.
    + apply× @isin_snd2. forwards*: H m Q0. nat_math.
      intros_all. forwards*: H3 b0. simpl_notin.
    + forwards*: H3 c. inverts× H4.
  - exp_ext c. inverts H4.
    + apply× @isin_par1. forwards*: H n0 P1. nat_math.
      intros_all. forwards*: H3 b0. simpl_notin.
    + apply× @isin_par2. forwards*: H m Q0. nat_math.
      intros_all. forwards*: H3 b0. simpl_notin.
  - ho_exp c P0. change_ext.
    constructor. intros. inverts H4.
    fresh_lp (a::c::b::nil) (nu P1 b). rename x into z'.
    apply isin_rename with z'; auto.
    change (isin b ((fun b ⇒ (P1 b z')) b)).
    eapply H; eauto.
    + nat_math.
    + intros_all. forwards*: H1 b0. simpl_notin.
    + intros_all. forwards*: H3 b0. simpl_notin.
Qed.

Lemma isin_arg {V:Set}: ∀ (P:name→proc V) a, notin_ho a P →
  isin a (P a) → ∀ b, isin b (P b).
Proof.
  intros. fresh_proc (nu P).
  destruct (exists_sz (P x)) as [n].
  apply isin_arg' with n (P x) x a; auto.
Qed.

Lemma unused_arg {V:Set} : ∀ (P:name → proc V) a,
  notin a (P a) → ∀ a b, P a = P b.
Proof.
  intros P a Hnotin.
  assert (notin_ho a P). { intros z Hz. apply notin_rename with a; auto. }
  induction (P a) eqn:HH; symmetry in HH; change_ext.
Qed.

Lemma notin_arg {V:Set} : ∀ (P:name → proc V) a,
  notin a (P a) → ∀ b, notin_ho b P → notin b (P b).
Proof.
  intros. destruct (isin_notin_dec b (P b)); auto.
  destruct (dec_name a b); subst; auto.
  forwards*: H0 a. rewrite (unused_arg P _ H a b) in H3; auto.
Qed.

Lemma list_of_proc {V:Set}: ∀ (P:proc V),
  ∃ L, ∀ a, ¬In a L → notin a P.
Proof.
  intro P; gen V. induction P; intros.
  - ∃ (@nil name); intros; auto with hopi.
  - destruct IHP as [L]. ∃ (n::L). intros.
    simpl_notin; auto with hopi.
  - destruct IHP1 as [L]. destruct IHP2 as [L'].
    ∃ (n::(L++L')). intros. simpl_notin; auto with hopi.
  - destruct IHP1 as [L]. destruct IHP2 as [L'].
    ∃ (L++L'). intros. simpl_notin; auto with hopi.
  - fresh_proc (nu p). forwards*: H x.
    destruct H0 as [Lx]. ∃ Lx. intros.
    constructor; intros. apply notin_rename with x; auto.
  - ∃ (@nil name); intros; auto with hopi.
Qed.


Inductive isinV {V:Set} : V → proc V → Prop :=
| isinV_var : ∀ v, isinV v (pr_var v)
| isinV_inp : ∀ a v P, @isinV (incV V) (VS v) P → isinV v (a ? P)
| isinV_snd1 : ∀ a v P Q, isinV v P → isinV v (a!(P) Q)
| isinV_snd2 : ∀ a v P Q, isinV v Q → isinV v (a!(P) Q)
| isinV_par1 : ∀ v P Q, isinV v P → isinV v (P // Q)
| isinV_par2 : ∀ v P Q, isinV v Q → isinV v (P // Q)
| isinV_nu : ∀ v P, (∀ z, isinV v (P z)) → isinV v (nu P).

Hint Constructors isinV:hopi.

Lemma isinV_rename' {V:Set}: ∀ n (Q:proc V),
      (size Q n) →
      ∀ P x, (notin_ho x P) → Q=(P x) →
      ∀ z v, (isinV v (P z)) →
      ∀ y, isinV v (P y).
Proof with nat_math.
  intro n; gen V.
  induction n using TLC.LibNat.peano_induction; intros.
  destruct Q; inverts H0; try solve [change_ext].
  - destruct (dec_name n0 x); subst; exp_ext x.
    + constructor. inverts H3. eapply H; eauto...
    + apply isinV_inp. inverts H3. eapply H; eauto...
  - destruct (dec_name n0 x); subst; exp_ext x.
    + inverts H3.
      × apply isinV_snd1. clear H0 H9. eapply H; eauto...
      × apply isinV_snd2. eapply H; eauto...
    + inverts H3.
      × apply isinV_snd1. clear H4 H9. eapply H; eauto...
      × apply isinV_snd2. eapply H; eauto...
  - exp_ext x. inverts H3.
    + apply isinV_par1. clear H8 H0. eapply H; eauto...
    + apply isinV_par2. eapply H; eauto...
  - ho_exp x p. rename p0 into P'. change_ext.
    clear H0. inverts H3. constructor. intros.
    fresh_lp (z0::x::nil) (nu P' y). rename x0 into z'.
    assert (isinV v (P' y z')).
    { change (isinV v ((fun y ⇒ P' y z') y)).
      eapply H; eauto. nat_math.
      intros_all. forwards*: H1 b. inverts H6.
      apply H9. auto. }
    assert (∀ x0, x0≠x → size (P' y x0) n0).
    { intros. change (size ((fun y ⇒ P' y x0) y) n0).
      eapply size_rename; eauto. intros_all. forwards*: H1 b.
      inverts H9. apply H11. auto. }
    
    clear H5. eapply H; eauto...
Qed.

Lemma isinV_rename {V:Set} : ∀ (P:name→proc V) x v, isinV v (P x) →
   ∀ y, isinV v (P y).
Proof.
  intros. fresh_proc (nu P).
  destruct (exists_sz (nu P)) as [n]. inverts H0.
  eapply isinV_rename'; eauto.
Qed.


Lemma notin_mapV {V W:Set} : ∀ (P:proc V) (f:V→W) a, notin a P → notin a (mapV f P).
Proof.
  intros_all. gen W. induction H; simpl; eauto with hopi.
Qed.

Lemma notin_mapV_rev {V W:Set} : ∀ (P:proc V) (f:V→W) a,
    notin a (mapV f P) → notin a P.
Proof.
  intros_all. gen W.
  induction P; intros; simpl_notin; constructor; auto;
    try solve [apply× IHP]; try solve [apply× IHP1]; try solve [apply× IHP2].
  intros. apply× H.
Qed.

Lemma notin_bind {V W:Set} : ∀ (P:proc V)(f:V→proc W) a,
  (∀ (v:V), isinV v P → notin a (f v)) →
  notin a P → notin a (bind f P).
Proof.
  intros; gen W.
  induction H0; simpl; eauto with hopi; intros; simpl_notin;
    constructor; default_simp; auto with hopi.
  + apply IHnotin; intros [|]; simpl; auto with hopi.
    intros. apply× @notin_mapV; auto with hopi.
  + apply× H0. intros. apply H1. constructor; auto.
    intros. eapply isinV_rename; eauto.
Qed.

Lemma notin_bind_rev {V W:Set} : ∀ (P:proc V)(f:V→proc W) a, notin a (bind f P) →
   (∀ v, isinV v P → notin a (f v)) ∧ notin a P.
Proof.
  intros. gen W. induction P; simpl; intuition (eauto with hopi);
    simpl_notin; try inverts H0; try inverts H1; try (constructor; auto);
    try solve [forwards*: IHP1 f]; try solve [forwards*: IHP2 f].
  - auto.
  - edestruct IHP. apply H4.
    forwards: H H2. simpl in H1. eapply notin_mapV_rev; eauto.
  - edestruct IHP; eauto.
  - fresh_list (a::nil). forwards*: H x.
  - intros. forwards*: H.
Qed.