Require Export fintype. Require Export header_extensible.
Section chan.
Inductive chan (nchan : nat) : Type :=
| var_chan : fin (nchan) -> chan (nchan).
Definition upRen_chan_chan { m : nat } { n : nat } (xi : fin (m) -> fin (n)) : fin (S m) -> fin (S n) :=
up_ren xi.
Definition ren_chan { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) (s : chan (mchan)) : chan (nchan) :=
match s with
| var_chan (_) s => (var_chan (nchan)) (xichan s)
end.
Definition upExtRen_chan_chan { m : nat } { n : nat } (xi : fin (m) -> fin (n)) (zeta : fin (m) -> fin (n)) (Eq : forall x, xi x = zeta x) : forall x, (upRen_chan_chan xi) x = (upRen_chan_chan zeta) x :=
fun n => match n with
| Some n => ap shift (Eq n)
| None => eq_refl
end.
Fixpoint extRen_chan { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) (zetachan : fin (mchan) -> fin (nchan)) (Eqchan : forall x, xichan x = zetachan x) (s : chan (mchan)) : ren_chan xichan s = ren_chan zetachan s
:=
match s with
| var_chan (_) s => ap (var_chan (nchan)) (Eqchan s)
end.
Definition up_ren_ren_chan_chan { k : nat } { l : nat } { m : nat } (xi : fin (k) -> fin (l)) (tau : fin (l) -> fin (m)) (theta : fin (k) -> fin (m)) (Eq : forall x, (funcomp tau xi) x = theta x) : forall x, (funcomp (upRen_chan_chan tau) (upRen_chan_chan xi)) x = (upRen_chan_chan theta) x :=
up_ren_ren xi tau theta Eq.
Fixpoint compRenRen_chan { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) (rhochan : fin (mchan) -> fin (lchan)) (Eqchan : forall x, (funcomp zetachan xichan) x = rhochan x) (s : chan (mchan)) : ren_chan zetachan (ren_chan xichan s) = ren_chan rhochan s :=
match s with
| var_chan (_) s => ap (var_chan (lchan)) (Eqchan s)
end.
Lemma varLRen_chan { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) : funcomp (ren_chan xichan) (var_chan (mchan)) = funcomp (var_chan (nchan)) xichan .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => eq_refl)). Qed.
Lemma renRen_chan { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) (s : chan (mchan)) : ren_chan zetachan (ren_chan xichan s) = ren_chan (funcomp zetachan xichan) s .
Proof. exact (compRenRen_chan xichan zetachan (_) (fun n => eq_refl) s). Qed.
Lemma renRen'_chan { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) : funcomp (ren_chan zetachan) (ren_chan xichan) = ren_chan (funcomp zetachan xichan) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n => renRen_chan xichan zetachan n)). Qed.
End chan.
Section proc.
Inductive proc (nchan : nat) : Type :=
| Nil : proc (nchan)
| Bang : proc (nchan) -> proc (nchan)
| Res : proc (S nchan) -> proc (nchan)
| Par : proc (nchan) -> proc (nchan) -> proc (nchan)
| In : chan (nchan) -> proc (S nchan) -> proc (nchan)
| Out : chan (nchan) -> chan (nchan) -> proc (nchan) -> proc (nchan).
Lemma congr_Nil { mchan : nat } : Nil (mchan) = Nil (mchan) .
Proof. congruence. Qed.
Lemma congr_Bang { mchan : nat } { s0 : proc (mchan) } { t0 : proc (mchan) } : s0 = t0 -> Bang (mchan) s0 = Bang (mchan) t0 .
Proof. congruence. Qed.
Lemma congr_Res { mchan : nat } { s0 : proc (S mchan) } { t0 : proc (S mchan) } : s0 = t0 -> Res (mchan) s0 = Res (mchan) t0 .
Proof. congruence. Qed.
Lemma congr_Par { mchan : nat } { s0 : proc (mchan) } { s1 : proc (mchan) } { t0 : proc (mchan) } { t1 : proc (mchan) } : s0 = t0 -> s1 = t1 -> Par (mchan) s0 s1 = Par (mchan) t0 t1 .
Proof. congruence. Qed.
Lemma congr_In { mchan : nat } { s0 : chan (mchan) } { s1 : proc (S mchan) } { t0 : chan (mchan) } { t1 : proc (S mchan) } : s0 = t0 -> s1 = t1 -> In (mchan) s0 s1 = In (mchan) t0 t1 .
Proof. congruence. Qed.
Lemma congr_Out { mchan : nat } { s0 : chan (mchan) } { s1 : chan (mchan) } { s2 : proc (mchan) } { t0 : chan (mchan) } { t1 : chan (mchan) } { t2 : proc (mchan) } : s0 = t0 -> s1 = t1 -> s2 = t2 -> Out (mchan) s0 s1 s2 = Out (mchan) t0 t1 t2 .
Proof. congruence. Qed.
Fixpoint ren_proc { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) (s : proc (mchan)) : proc (nchan) :=
match s with
| Nil (_) => Nil (nchan)
| Bang (_) s0 => Bang (nchan) (ren_proc xichan s0)
| Res (_) s0 => Res (nchan) (ren_proc (upRen_chan_chan xichan) s0)
| Par (_) s0 s1 => Par (nchan) (ren_proc xichan s0) (ren_proc xichan s1)
| In (_) s0 s1 => In (nchan) (ren_chan xichan s0) (ren_proc (upRen_chan_chan xichan) s1)
| Out (_) s0 s1 s2 => Out (nchan) (ren_chan xichan s0) (ren_chan xichan s1) (ren_proc xichan s2)
end.
Fixpoint extRen_proc { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) (zetachan : fin (mchan) -> fin (nchan)) (Eqchan : forall x, xichan x = zetachan x) (s : proc (mchan)) : ren_proc xichan s = ren_proc zetachan s :=
match s with
| Nil (_) => congr_Nil
| Bang (_) s0 => congr_Bang (extRen_proc xichan zetachan Eqchan s0)
| Res (_) s0 => congr_Res (extRen_proc (upRen_chan_chan xichan) (upRen_chan_chan zetachan) (upExtRen_chan_chan (_) (_) Eqchan) s0)
| Par (_) s0 s1 => congr_Par (extRen_proc xichan zetachan Eqchan s0) (extRen_proc xichan zetachan Eqchan s1)
| In (_) s0 s1 => congr_In (extRen_chan xichan zetachan Eqchan s0) (extRen_proc (upRen_chan_chan xichan) (upRen_chan_chan zetachan) (upExtRen_chan_chan (_) (_) Eqchan) s1)
| Out (_) s0 s1 s2 => congr_Out (extRen_chan xichan zetachan Eqchan s0) (extRen_chan xichan zetachan Eqchan s1) (extRen_proc xichan zetachan Eqchan s2)
end.
Fixpoint compRenRen_proc { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) (rhochan : fin (mchan) -> fin (lchan)) (Eqchan : forall x, (funcomp zetachan xichan) x = rhochan x) (s : proc (mchan)) : ren_proc zetachan (ren_proc xichan s) = ren_proc rhochan s :=
match s with
| Nil (_) => congr_Nil
| Bang (_) s0 => congr_Bang (compRenRen_proc xichan zetachan rhochan Eqchan s0)
| Res (_) s0 => congr_Res (compRenRen_proc (upRen_chan_chan xichan) (upRen_chan_chan zetachan) (upRen_chan_chan rhochan) (up_ren_ren_chan_chan (_) (_) (_) Eqchan) s0)
| Par (_) s0 s1 => congr_Par (compRenRen_proc xichan zetachan rhochan Eqchan s0) (compRenRen_proc xichan zetachan rhochan Eqchan s1)
| In (_) s0 s1 => congr_In (compRenRen_chan xichan zetachan rhochan Eqchan s0) (compRenRen_proc (upRen_chan_chan xichan) (upRen_chan_chan zetachan) (upRen_chan_chan rhochan) (up_ren_ren_chan_chan (_) (_) (_) Eqchan) s1)
| Out (_) s0 s1 s2 => congr_Out (compRenRen_chan xichan zetachan rhochan Eqchan s0) (compRenRen_chan xichan zetachan rhochan Eqchan s1) (compRenRen_proc xichan zetachan rhochan Eqchan s2)
end.
Lemma renRen_proc { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) (s : proc (mchan)) : ren_proc zetachan (ren_proc xichan s) = ren_proc (funcomp zetachan xichan) s .
Proof. exact (compRenRen_proc xichan zetachan (_) (fun n => eq_refl) s). Qed.
Lemma renRen'_proc { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) : funcomp (ren_proc zetachan) (ren_proc xichan) = ren_proc (funcomp zetachan xichan) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n => renRen_proc xichan zetachan n)). Qed.
End proc.
Arguments var_chan {nchan}.
Arguments Nil {nchan}.
Arguments Bang {nchan}.
Arguments Res {nchan}.
Arguments Par {nchan}.
Arguments In {nchan}.
Arguments Out {nchan}.
Global Instance Ren_chan { mchan : nat } { nchan : nat } : Ren1 (fin (mchan) -> fin (nchan)) (chan (mchan)) (chan (nchan)) := @ren_chan (mchan) (nchan) .
Global Instance Ren_proc { mchan : nat } { nchan : nat } : Ren1 (fin (mchan) -> fin (nchan)) (proc (mchan)) (proc (nchan)) := @ren_proc (mchan) (nchan) .
Global Instance VarInstance_chan { mchan : nat } : Var (fin (mchan)) (chan (mchan)) := @var_chan (mchan) .
Notation "x '__chan'" := (var_chan x) (at level 5, format "x __chan") : subst_scope.
Notation "x '__chan'" := (@ids (_) (_) VarInstance_chan x) (at level 5, only printing, format "x __chan") : subst_scope.
Notation "'var'" := (var_chan) (only printing, at level 1) : subst_scope.
Class Up_chan X Y := up_chan : X -> Y.
Notation "↑__chan" := (up_chan) (only printing) : subst_scope.
Notation "s ⟨ xichan ⟩" := (ren_chan xichan s) (at level 7, left associativity, only printing) : subst_scope.
Notation "⟨ xichan ⟩" := (ren_chan xichan) (at level 1, left associativity, only printing) : fscope.
Notation "s ⟨ xichan ⟩" := (ren_proc xichan s) (at level 7, left associativity, only printing) : subst_scope.
Notation "⟨ xichan ⟩" := (ren_proc xichan) (at level 1, left associativity, only printing) : fscope.
Ltac auto_unfold := repeat unfold subst1, ren1, subst2, ren2, Subst1, Ren1, Subst2, Ren2, ids, Ren_chan, Ren_proc, VarInstance_chan.
Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, ren1, subst2, ren2, Subst1, Ren1, Subst2, Ren2, ids, Ren_chan, Ren_proc, VarInstance_chan in *.
Ltac asimpl' := repeat first [ progress rewrite ?renRen_chan| progress rewrite ?renRen'_chan| progress rewrite ?renRen_proc| progress rewrite ?renRen'_proc| progress (unfold up_ren, upRen_chan_chan)| progress (cbn [ren_chan ren_proc])| fsimpl].
Ltac asimpl := repeat try unfold_funcomp; auto_unfold in *; asimpl'; repeat try unfold_funcomp.
Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.
Tactic Notation "auto_case" := auto_case (asimpl; cbn; eauto).
Tactic Notation "asimpl" "in" "*" := auto_unfold in *; repeat first [ progress rewrite ?renRen_chan in *| progress rewrite ?renRen'_chan in *| progress rewrite ?renRen_proc in *| progress rewrite ?renRen'_proc in *| progress (unfold up_ren, upRen_chan_chan in *)| progress (cbn [ren_chan ren_proc] in *)| fsimpl in *].
Section chan.
Inductive chan (nchan : nat) : Type :=
| var_chan : fin (nchan) -> chan (nchan).
Definition upRen_chan_chan { m : nat } { n : nat } (xi : fin (m) -> fin (n)) : fin (S m) -> fin (S n) :=
up_ren xi.
Definition ren_chan { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) (s : chan (mchan)) : chan (nchan) :=
match s with
| var_chan (_) s => (var_chan (nchan)) (xichan s)
end.
Definition upExtRen_chan_chan { m : nat } { n : nat } (xi : fin (m) -> fin (n)) (zeta : fin (m) -> fin (n)) (Eq : forall x, xi x = zeta x) : forall x, (upRen_chan_chan xi) x = (upRen_chan_chan zeta) x :=
fun n => match n with
| Some n => ap shift (Eq n)
| None => eq_refl
end.
Fixpoint extRen_chan { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) (zetachan : fin (mchan) -> fin (nchan)) (Eqchan : forall x, xichan x = zetachan x) (s : chan (mchan)) : ren_chan xichan s = ren_chan zetachan s
:=
match s with
| var_chan (_) s => ap (var_chan (nchan)) (Eqchan s)
end.
Definition up_ren_ren_chan_chan { k : nat } { l : nat } { m : nat } (xi : fin (k) -> fin (l)) (tau : fin (l) -> fin (m)) (theta : fin (k) -> fin (m)) (Eq : forall x, (funcomp tau xi) x = theta x) : forall x, (funcomp (upRen_chan_chan tau) (upRen_chan_chan xi)) x = (upRen_chan_chan theta) x :=
up_ren_ren xi tau theta Eq.
Fixpoint compRenRen_chan { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) (rhochan : fin (mchan) -> fin (lchan)) (Eqchan : forall x, (funcomp zetachan xichan) x = rhochan x) (s : chan (mchan)) : ren_chan zetachan (ren_chan xichan s) = ren_chan rhochan s :=
match s with
| var_chan (_) s => ap (var_chan (lchan)) (Eqchan s)
end.
Lemma varLRen_chan { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) : funcomp (ren_chan xichan) (var_chan (mchan)) = funcomp (var_chan (nchan)) xichan .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => eq_refl)). Qed.
Lemma renRen_chan { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) (s : chan (mchan)) : ren_chan zetachan (ren_chan xichan s) = ren_chan (funcomp zetachan xichan) s .
Proof. exact (compRenRen_chan xichan zetachan (_) (fun n => eq_refl) s). Qed.
Lemma renRen'_chan { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) : funcomp (ren_chan zetachan) (ren_chan xichan) = ren_chan (funcomp zetachan xichan) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n => renRen_chan xichan zetachan n)). Qed.
End chan.
Section proc.
Inductive proc (nchan : nat) : Type :=
| Nil : proc (nchan)
| Bang : proc (nchan) -> proc (nchan)
| Res : proc (S nchan) -> proc (nchan)
| Par : proc (nchan) -> proc (nchan) -> proc (nchan)
| In : chan (nchan) -> proc (S nchan) -> proc (nchan)
| Out : chan (nchan) -> chan (nchan) -> proc (nchan) -> proc (nchan).
Lemma congr_Nil { mchan : nat } : Nil (mchan) = Nil (mchan) .
Proof. congruence. Qed.
Lemma congr_Bang { mchan : nat } { s0 : proc (mchan) } { t0 : proc (mchan) } : s0 = t0 -> Bang (mchan) s0 = Bang (mchan) t0 .
Proof. congruence. Qed.
Lemma congr_Res { mchan : nat } { s0 : proc (S mchan) } { t0 : proc (S mchan) } : s0 = t0 -> Res (mchan) s0 = Res (mchan) t0 .
Proof. congruence. Qed.
Lemma congr_Par { mchan : nat } { s0 : proc (mchan) } { s1 : proc (mchan) } { t0 : proc (mchan) } { t1 : proc (mchan) } : s0 = t0 -> s1 = t1 -> Par (mchan) s0 s1 = Par (mchan) t0 t1 .
Proof. congruence. Qed.
Lemma congr_In { mchan : nat } { s0 : chan (mchan) } { s1 : proc (S mchan) } { t0 : chan (mchan) } { t1 : proc (S mchan) } : s0 = t0 -> s1 = t1 -> In (mchan) s0 s1 = In (mchan) t0 t1 .
Proof. congruence. Qed.
Lemma congr_Out { mchan : nat } { s0 : chan (mchan) } { s1 : chan (mchan) } { s2 : proc (mchan) } { t0 : chan (mchan) } { t1 : chan (mchan) } { t2 : proc (mchan) } : s0 = t0 -> s1 = t1 -> s2 = t2 -> Out (mchan) s0 s1 s2 = Out (mchan) t0 t1 t2 .
Proof. congruence. Qed.
Fixpoint ren_proc { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) (s : proc (mchan)) : proc (nchan) :=
match s with
| Nil (_) => Nil (nchan)
| Bang (_) s0 => Bang (nchan) (ren_proc xichan s0)
| Res (_) s0 => Res (nchan) (ren_proc (upRen_chan_chan xichan) s0)
| Par (_) s0 s1 => Par (nchan) (ren_proc xichan s0) (ren_proc xichan s1)
| In (_) s0 s1 => In (nchan) (ren_chan xichan s0) (ren_proc (upRen_chan_chan xichan) s1)
| Out (_) s0 s1 s2 => Out (nchan) (ren_chan xichan s0) (ren_chan xichan s1) (ren_proc xichan s2)
end.
Fixpoint extRen_proc { mchan : nat } { nchan : nat } (xichan : fin (mchan) -> fin (nchan)) (zetachan : fin (mchan) -> fin (nchan)) (Eqchan : forall x, xichan x = zetachan x) (s : proc (mchan)) : ren_proc xichan s = ren_proc zetachan s :=
match s with
| Nil (_) => congr_Nil
| Bang (_) s0 => congr_Bang (extRen_proc xichan zetachan Eqchan s0)
| Res (_) s0 => congr_Res (extRen_proc (upRen_chan_chan xichan) (upRen_chan_chan zetachan) (upExtRen_chan_chan (_) (_) Eqchan) s0)
| Par (_) s0 s1 => congr_Par (extRen_proc xichan zetachan Eqchan s0) (extRen_proc xichan zetachan Eqchan s1)
| In (_) s0 s1 => congr_In (extRen_chan xichan zetachan Eqchan s0) (extRen_proc (upRen_chan_chan xichan) (upRen_chan_chan zetachan) (upExtRen_chan_chan (_) (_) Eqchan) s1)
| Out (_) s0 s1 s2 => congr_Out (extRen_chan xichan zetachan Eqchan s0) (extRen_chan xichan zetachan Eqchan s1) (extRen_proc xichan zetachan Eqchan s2)
end.
Fixpoint compRenRen_proc { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) (rhochan : fin (mchan) -> fin (lchan)) (Eqchan : forall x, (funcomp zetachan xichan) x = rhochan x) (s : proc (mchan)) : ren_proc zetachan (ren_proc xichan s) = ren_proc rhochan s :=
match s with
| Nil (_) => congr_Nil
| Bang (_) s0 => congr_Bang (compRenRen_proc xichan zetachan rhochan Eqchan s0)
| Res (_) s0 => congr_Res (compRenRen_proc (upRen_chan_chan xichan) (upRen_chan_chan zetachan) (upRen_chan_chan rhochan) (up_ren_ren_chan_chan (_) (_) (_) Eqchan) s0)
| Par (_) s0 s1 => congr_Par (compRenRen_proc xichan zetachan rhochan Eqchan s0) (compRenRen_proc xichan zetachan rhochan Eqchan s1)
| In (_) s0 s1 => congr_In (compRenRen_chan xichan zetachan rhochan Eqchan s0) (compRenRen_proc (upRen_chan_chan xichan) (upRen_chan_chan zetachan) (upRen_chan_chan rhochan) (up_ren_ren_chan_chan (_) (_) (_) Eqchan) s1)
| Out (_) s0 s1 s2 => congr_Out (compRenRen_chan xichan zetachan rhochan Eqchan s0) (compRenRen_chan xichan zetachan rhochan Eqchan s1) (compRenRen_proc xichan zetachan rhochan Eqchan s2)
end.
Lemma renRen_proc { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) (s : proc (mchan)) : ren_proc zetachan (ren_proc xichan s) = ren_proc (funcomp zetachan xichan) s .
Proof. exact (compRenRen_proc xichan zetachan (_) (fun n => eq_refl) s). Qed.
Lemma renRen'_proc { kchan : nat } { lchan : nat } { mchan : nat } (xichan : fin (mchan) -> fin (kchan)) (zetachan : fin (kchan) -> fin (lchan)) : funcomp (ren_proc zetachan) (ren_proc xichan) = ren_proc (funcomp zetachan xichan) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n => renRen_proc xichan zetachan n)). Qed.
End proc.
Arguments var_chan {nchan}.
Arguments Nil {nchan}.
Arguments Bang {nchan}.
Arguments Res {nchan}.
Arguments Par {nchan}.
Arguments In {nchan}.
Arguments Out {nchan}.
Global Instance Ren_chan { mchan : nat } { nchan : nat } : Ren1 (fin (mchan) -> fin (nchan)) (chan (mchan)) (chan (nchan)) := @ren_chan (mchan) (nchan) .
Global Instance Ren_proc { mchan : nat } { nchan : nat } : Ren1 (fin (mchan) -> fin (nchan)) (proc (mchan)) (proc (nchan)) := @ren_proc (mchan) (nchan) .
Global Instance VarInstance_chan { mchan : nat } : Var (fin (mchan)) (chan (mchan)) := @var_chan (mchan) .
Notation "x '__chan'" := (var_chan x) (at level 5, format "x __chan") : subst_scope.
Notation "x '__chan'" := (@ids (_) (_) VarInstance_chan x) (at level 5, only printing, format "x __chan") : subst_scope.
Notation "'var'" := (var_chan) (only printing, at level 1) : subst_scope.
Class Up_chan X Y := up_chan : X -> Y.
Notation "↑__chan" := (up_chan) (only printing) : subst_scope.
Notation "s ⟨ xichan ⟩" := (ren_chan xichan s) (at level 7, left associativity, only printing) : subst_scope.
Notation "⟨ xichan ⟩" := (ren_chan xichan) (at level 1, left associativity, only printing) : fscope.
Notation "s ⟨ xichan ⟩" := (ren_proc xichan s) (at level 7, left associativity, only printing) : subst_scope.
Notation "⟨ xichan ⟩" := (ren_proc xichan) (at level 1, left associativity, only printing) : fscope.
Ltac auto_unfold := repeat unfold subst1, ren1, subst2, ren2, Subst1, Ren1, Subst2, Ren2, ids, Ren_chan, Ren_proc, VarInstance_chan.
Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, ren1, subst2, ren2, Subst1, Ren1, Subst2, Ren2, ids, Ren_chan, Ren_proc, VarInstance_chan in *.
Ltac asimpl' := repeat first [ progress rewrite ?renRen_chan| progress rewrite ?renRen'_chan| progress rewrite ?renRen_proc| progress rewrite ?renRen'_proc| progress (unfold up_ren, upRen_chan_chan)| progress (cbn [ren_chan ren_proc])| fsimpl].
Ltac asimpl := repeat try unfold_funcomp; auto_unfold in *; asimpl'; repeat try unfold_funcomp.
Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.
Tactic Notation "auto_case" := auto_case (asimpl; cbn; eauto).
Tactic Notation "asimpl" "in" "*" := auto_unfold in *; repeat first [ progress rewrite ?renRen_chan in *| progress rewrite ?renRen'_chan in *| progress rewrite ?renRen_proc in *| progress rewrite ?renRen'_proc in *| progress (unfold up_ren, upRen_chan_chan in *)| progress (cbn [ren_chan ren_proc] in *)| fsimpl in *].