SysF_PTS.lib
Require Import Lt Le List Compare_dec Plus Minus EqNat Bool Omega Program.Equality.
From Autosubst Require Export Autosubst.
Require Export Decidable.
Ltac atom_ren :=
(repeat
match goal with
| [H : ?T = ?S.[ren ?xi] |- _] => (destruct S; simpl in H; try discriminate H);[idtac]; try match goal with [H : T = T |- _] => clear H end
| [H : ?S.[ren ?xi] = ?T |- _] => (destruct S; simpl in H; try discriminate H);[idtac]; try match goal with [H : T = T |- _] => clear H
end
end); ainv.
Class Functor (F : Type -> Type) := {fmap {X Y} : (X -> Y) -> F X -> F Y}.
Infix "<$>" := fmap (left associativity, at level 11).
Class Monad (m : Type -> Type) :=
{
bind {X Y} : m X -> (X -> m Y) -> m Y;
ret {X} : X -> m X
}.
Notation "'do' x <- a ; s" := (bind a (fun x => s)) (right associativity, at level 100).
Notation "'GET' x <- a ; P" := (match a with Some x => P | _ => False end) (right associativity, at level 100).
Instance Functor_Monad {m} {_ : Monad m} : Functor m :=
{ fmap X Y f a := do a' <- a; ret(f a') }.
Instance : Monad option :=
{
bind X Y a f := match a with None => None | Some a' => f a' end;
ret := Some
}.
Lemma decide_refl {X Y} (a : X) (_ : Dec (a = a)) (s t : Y) : (if decide (a = a) then s else t) = s.
Proof. decide (a = a); congruence. Qed.
Ltac simpG := simpl in *; repeat match goal with
| [H : context[if decide (?s = ?s) then _ else _] |- _] => rewrite decide_refl in H
end.
Ltac ca := simpG; repeat match goal with
| [|- context[match ?s with _ => _ end]] => ( assert True as _; (destruct s eqn:?; simpG; try contradiction; try congruence; eauto)); [trivial | fail..]
| [H : context[match ?s with _ => _ end] |- _] => ( assert True as _; (destruct s eqn:?; simpG; try contradiction; try congruence; eauto)); [trivial | fail..]
end.
Ltac clean_goal := repeat
match goal with
[H : ?s = ?s |- _] => clear H
| [H : ?T |- _] => match T with _ /\ _ => idtac | (_,_) => idtac end; destruct H
end.
Ltac autodestr := repeat (clean_goal; try subst; simpl; match goal with [|- context[match ?s with _ => _ end]] =>
try match s with context[match _ with _ => _ end] => fail 2 end;
destruct s eqn:? end); try subst; simpl; trivial.
Ltac subst' := repeat progress match goal with [x : _ |- _] => subst x end.
Ltac clear_rec := first[subst | match goal with [H : _ = _ |- _] => clear H; subst end].
Tactic Notation "getH" open_constr(T) := match goal with [H : context[T] |- _] => exact H end.
Notation "$$( T )" := ltac:(getH T).
Notation "$?" := ltac:(eauto; econstructor; try econstructor; now eauto) (only parsing).
Ltac aspec := repeat match goal with
| [H : _ |- _] => first[ specialize (H _ _ _ $?) | specialize (H _ _ $?) | specialize (H $?) | specialize (H _ $?) ] end.
Notation "(-1)" := (0 .: id).
Definition sum2bool {A B} (x : A + B) := if x then true else false.
Coercion sum2bool : sum >-> bool.
Definition comb {X Y} (bits : X -> bool) f g x : Y := if bits x then f x else g x.
Arguments comb {X Y} bits f g x/.
Lemma comb_cons {X} bits (sigma tau : var -> X) : comb bits sigma tau = (if bits 0 then sigma 0 else tau 0) .: comb ((+1) >>> bits) ((+1) >>> sigma) ((+1) >>> tau).
Proof. f_ext. intros [|]; reflexivity. Qed.
Lemma comb_comp {A B C} (bits : A -> bool) sigma tau (f : B -> C) : comb bits sigma tau >>> f = comb bits (sigma >>> f) (tau >>> f).
Proof. f_ext; intros. simpl. destruct (bits x); reflexivity. Qed.
Lemma upren_comb bits xi zeta b : upren (comb bits xi zeta) = comb (b .: bits) (upren xi) (upren zeta).
Proof. setoid_rewrite comb_cons at 2. destruct b; asimpl; unfold upren; now rewrite comb_comp. Qed.
(* Q-JK: before now: both S and (+1) appear in goal *)
Section SubstInstance.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}
{Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}.
(* standard context lookup *)
Inductive atn: list term -> var -> term -> Prop :=
| Atn0 Delta A : atn (A :: Delta) 0 A
| AtnS Delta x A B :
atn Delta x B -> atn (A :: Delta) (S x) B.
Fixpoint get Gamma {struct Gamma} : var -> option term :=
match Gamma with
| nil => (fun n => None)
| s :: Gamma => Some s .: get Gamma
end.
Lemma get_atn Gamma n s : get Gamma n = Some s -> atn Gamma n s.
Proof.
revert n s. induction Gamma; intros n s E.
- inversion E.
- destruct n as [|n]; simpl in E.
+ inversion E; subst. constructor.
+ constructor; auto.
Qed.
Lemma atn_get Gamma n s : atn Gamma n s -> get Gamma n = Some s.
Proof. induction 1; intros; subst; simpl; now autorew. Qed.
Lemma mmap_atn {f : term -> term} {Gamma x A'} :
atn (mmap f Gamma) x A' -> exists A, A' = (f A) /\ atn Gamma x A.
Proof.
intros H. depind H.
- destruct Gamma; ainv. eexists. eauto using atn.
- destruct Gamma; try now ainv.
simpl in x.
inversion x.
destruct (IHatn _ _ _ $$(Gamma)) as [ B' [H_eq H_atn]].
exists B'. eauto using atn.
Qed.
Lemma atn_mmap {f : term -> term} {Gamma x A A'} :
atn Gamma x A -> A' = (f A) -> atn (mmap f Gamma) x A'.
Proof. induction 1; intros; subst; constructor; eauto. Qed.
Lemma mmap_get {f : term -> term} {Gamma x A'} :
get (mmap f Gamma) x = Some A' -> exists A, A' = (f A) /\ get Gamma x = Some A.
Proof.
intros H. apply get_atn in H. destruct (mmap_atn H) as [A [EA H']].
exists A; eauto using atn_get.
Qed.
Lemma get_mmap {f : term -> term} {Gamma x A A'} :
get Gamma x = Some A -> A' = (f A) -> get (mmap f Gamma) x = Some A'.
Proof. intros. apply atn_get. apply get_atn in H. eapply atn_mmap; eauto. Qed.
Lemma mmap_get_None {f : term -> term} {Gamma x} :
get (mmap f Gamma) x = None -> get Gamma x = None.
Proof.
intros H. case_eq (get Gamma x); trivial. intros t Et. exfalso.
eapply @get_mmap with (f:=f) in Et; eauto. congruence.
Qed.
Lemma get_mmap_None {f : term -> term} {Gamma x} :
get Gamma x = None -> get (mmap f Gamma) x = None.
Proof.
intros H. case_eq (get (mmap f Gamma) x); trivial. intros t Et. exfalso.
destruct (mmap_get Et) as [s [_ H']]. congruence.
Qed.
(* dependent context lookup *)
Inductive atnd: list term -> var -> term -> Prop :=
| Atnd0 Delta A A' :
A' = A.[ren(+1)] -> atnd (A :: Delta) 0 A'
| AtndS Delta x A B B' :
atnd Delta x B -> B' = B.[ren(+1)] -> atnd (A :: Delta) (S x) B'.
Fixpoint getD (Gamma : list term) n : option term :=
match Gamma with
| nil => fun n => None
| s :: Gamma => Some s.[ren(+1)] .: getD Gamma >>> fmap(subst(ren(+1)))
end n.
Arguments getD !Gamma/ n.
Lemma getD_atnd Gamma n s : getD Gamma n = Some s -> atnd Gamma n s.
Proof.
revert n s. induction Gamma; intros n s E.
- inversion E.
- destruct n as [|n].
+ simpl in E. inversion E; subst. now constructor.
+ simpl in E. case_eq (getD Gamma n); [intros t E'|intros E']; rewrite E' in E; inversion E; subst.
econstructor; eauto.
Qed.
Lemma atnd_getD Gamma n s : atnd Gamma n s -> getD Gamma n = Some s.
Proof. induction 1; intros; subst; simpl; now autorew. Qed.
(* Connecting the two notions *)
Lemma getD_get Gamma n : getD Gamma n = subst (ren(+S n)) <$> (get Gamma n).
Proof.
revert Gamma; induction n; intros; destruct Gamma; simpl; autorew; trivial.
asimpl. autodestr. autosubst.
Qed.
Lemma getD_cons (s : term) (Gamma : list term) :
getD (s :: Gamma) = (Some s.[ren (+1)]) .: getD Gamma..[ren (+1)].
Proof.
f_ext. intros [|n]; trivial. rewrite getD_get.
replace ((Some s.[ren (+1)] .: getD Gamma..[ren (+1)]) (S n)) with (getD Gamma..[ren (+1)] n) by reflexivity.
repeat rewrite getD_get. asimpl.
case_eq (get Gamma n).
- intros t Et.
assert (E: get Gamma..[ren (+1)] n = Some t.[ren (+1)]) by (eapply get_mmap; eauto).
rewrite E; autosubst.
- intros E. rewrite get_mmap_None; trivial.
Qed.
End SubstInstance.
(* Generic context renamings *)
Section ContextRenamings.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}
{Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}.
Definition cr xi Gamma Delta := forall n t, atnd Gamma n t -> atnd Delta (xi n) t.[ren xi].
Lemma cr_up t xi Gamma Delta : cr xi Gamma Delta -> cr (upren xi) (t :: Gamma) (t.[ren xi] :: Delta).
Proof. intros c [|] s l; inversion l; subst; econstructor; eauto; autosubst. Qed.
Lemma cr_shift Gamma t : cr (+1) Gamma (t :: Gamma).
Proof. intros n s l. asimpl. econstructor; eauto. Qed.
End ContextRenamings.
Section CtxBoolFun.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}.
Definition bfr (xi : var -> var) delta gamma := forall n, gamma n = true -> delta (xi n) = true.
Lemma bfr_up b xi delta gamma : bfr xi delta gamma -> bfr (upren xi) (b .: delta) (b .: gamma).
Proof. intros H [|n] e; asimpl; eauto. Qed.
Lemma bfr_shift b gamma : bfr (+1) (b .: gamma) gamma.
Proof. intros n e. trivial. Qed.
Lemma bfr_ushift gamma : bfr (-1) gamma (false .: gamma).
Proof. intros [|n]; asimpl; trivial. discriminate. Qed.
End CtxBoolFun.
Section Coincidence.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}
{Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}.
Definition subst_coinc (gamma : var -> bool) (sigma tau : var -> term) := forall n, gamma n = true -> sigma n = tau n.
Lemma subst_coinc_id gamma sigma : subst_coinc gamma sigma sigma.
Proof. now intros n. Qed.
Lemma subst_coinc_up b gamma sigma tau : subst_coinc gamma sigma tau -> subst_coinc (b .: gamma) (up sigma) (up tau).
Proof. intros H [|n] A; asimpl in *; trivial. now rewrite H. Qed.
(* Lemma ren_coinc_hd_f b gamma xi zeta : b = false -> subst_coinc gamma (ren xi) tau -> subst_coinc (b .: gamma) (ren (x .: xi)) (ren (z .: zeta)). *)
(* Proof. intros E H |n A; asimpl in *; try congruence. now apply H. Qed. *)
Lemma subst_coinc_hd_f b gamma sigma tau : b = false -> subst_coinc gamma ((+1) >>> sigma) ((+1) >>> tau) -> subst_coinc (b .: gamma) sigma tau.
Proof. intros E H [|n] A; asimpl in *; try congruence. now apply (H n). Qed.
End Coincidence.
Section CoincidenceHSubst.
Context {type : Type}.
Context {Ids_type : Ids type} {Rename_type : Rename type}
{Subst_type : Subst type} {SubstLemmas_type : SubstLemmas type}.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}
{Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}
{HSubst_term : HSubst type term} {HSubstLemmas_term : HSubstLemmas type term}.
Lemma subst_coinc_hcomp gamma sigma tau rho : subst_coinc gamma sigma tau -> subst_coinc gamma (sigma >>| rho) (tau >>| rho).
Proof. intros H n E. asimpl. f_equal. eauto. Qed.
End CoincidenceHSubst.
From Autosubst Require Export Autosubst.
Require Export Decidable.
Ltac atom_ren :=
(repeat
match goal with
| [H : ?T = ?S.[ren ?xi] |- _] => (destruct S; simpl in H; try discriminate H);[idtac]; try match goal with [H : T = T |- _] => clear H end
| [H : ?S.[ren ?xi] = ?T |- _] => (destruct S; simpl in H; try discriminate H);[idtac]; try match goal with [H : T = T |- _] => clear H
end
end); ainv.
Class Functor (F : Type -> Type) := {fmap {X Y} : (X -> Y) -> F X -> F Y}.
Infix "<$>" := fmap (left associativity, at level 11).
Class Monad (m : Type -> Type) :=
{
bind {X Y} : m X -> (X -> m Y) -> m Y;
ret {X} : X -> m X
}.
Notation "'do' x <- a ; s" := (bind a (fun x => s)) (right associativity, at level 100).
Notation "'GET' x <- a ; P" := (match a with Some x => P | _ => False end) (right associativity, at level 100).
Instance Functor_Monad {m} {_ : Monad m} : Functor m :=
{ fmap X Y f a := do a' <- a; ret(f a') }.
Instance : Monad option :=
{
bind X Y a f := match a with None => None | Some a' => f a' end;
ret := Some
}.
Lemma decide_refl {X Y} (a : X) (_ : Dec (a = a)) (s t : Y) : (if decide (a = a) then s else t) = s.
Proof. decide (a = a); congruence. Qed.
Ltac simpG := simpl in *; repeat match goal with
| [H : context[if decide (?s = ?s) then _ else _] |- _] => rewrite decide_refl in H
end.
Ltac ca := simpG; repeat match goal with
| [|- context[match ?s with _ => _ end]] => ( assert True as _; (destruct s eqn:?; simpG; try contradiction; try congruence; eauto)); [trivial | fail..]
| [H : context[match ?s with _ => _ end] |- _] => ( assert True as _; (destruct s eqn:?; simpG; try contradiction; try congruence; eauto)); [trivial | fail..]
end.
Ltac clean_goal := repeat
match goal with
[H : ?s = ?s |- _] => clear H
| [H : ?T |- _] => match T with _ /\ _ => idtac | (_,_) => idtac end; destruct H
end.
Ltac autodestr := repeat (clean_goal; try subst; simpl; match goal with [|- context[match ?s with _ => _ end]] =>
try match s with context[match _ with _ => _ end] => fail 2 end;
destruct s eqn:? end); try subst; simpl; trivial.
Ltac subst' := repeat progress match goal with [x : _ |- _] => subst x end.
Ltac clear_rec := first[subst | match goal with [H : _ = _ |- _] => clear H; subst end].
Tactic Notation "getH" open_constr(T) := match goal with [H : context[T] |- _] => exact H end.
Notation "$$( T )" := ltac:(getH T).
Notation "$?" := ltac:(eauto; econstructor; try econstructor; now eauto) (only parsing).
Ltac aspec := repeat match goal with
| [H : _ |- _] => first[ specialize (H _ _ _ $?) | specialize (H _ _ $?) | specialize (H $?) | specialize (H _ $?) ] end.
Notation "(-1)" := (0 .: id).
Definition sum2bool {A B} (x : A + B) := if x then true else false.
Coercion sum2bool : sum >-> bool.
Definition comb {X Y} (bits : X -> bool) f g x : Y := if bits x then f x else g x.
Arguments comb {X Y} bits f g x/.
Lemma comb_cons {X} bits (sigma tau : var -> X) : comb bits sigma tau = (if bits 0 then sigma 0 else tau 0) .: comb ((+1) >>> bits) ((+1) >>> sigma) ((+1) >>> tau).
Proof. f_ext. intros [|]; reflexivity. Qed.
Lemma comb_comp {A B C} (bits : A -> bool) sigma tau (f : B -> C) : comb bits sigma tau >>> f = comb bits (sigma >>> f) (tau >>> f).
Proof. f_ext; intros. simpl. destruct (bits x); reflexivity. Qed.
Lemma upren_comb bits xi zeta b : upren (comb bits xi zeta) = comb (b .: bits) (upren xi) (upren zeta).
Proof. setoid_rewrite comb_cons at 2. destruct b; asimpl; unfold upren; now rewrite comb_comp. Qed.
(* Q-JK: before now: both S and (+1) appear in goal *)
Section SubstInstance.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}
{Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}.
(* standard context lookup *)
Inductive atn: list term -> var -> term -> Prop :=
| Atn0 Delta A : atn (A :: Delta) 0 A
| AtnS Delta x A B :
atn Delta x B -> atn (A :: Delta) (S x) B.
Fixpoint get Gamma {struct Gamma} : var -> option term :=
match Gamma with
| nil => (fun n => None)
| s :: Gamma => Some s .: get Gamma
end.
Lemma get_atn Gamma n s : get Gamma n = Some s -> atn Gamma n s.
Proof.
revert n s. induction Gamma; intros n s E.
- inversion E.
- destruct n as [|n]; simpl in E.
+ inversion E; subst. constructor.
+ constructor; auto.
Qed.
Lemma atn_get Gamma n s : atn Gamma n s -> get Gamma n = Some s.
Proof. induction 1; intros; subst; simpl; now autorew. Qed.
Lemma mmap_atn {f : term -> term} {Gamma x A'} :
atn (mmap f Gamma) x A' -> exists A, A' = (f A) /\ atn Gamma x A.
Proof.
intros H. depind H.
- destruct Gamma; ainv. eexists. eauto using atn.
- destruct Gamma; try now ainv.
simpl in x.
inversion x.
destruct (IHatn _ _ _ $$(Gamma)) as [ B' [H_eq H_atn]].
exists B'. eauto using atn.
Qed.
Lemma atn_mmap {f : term -> term} {Gamma x A A'} :
atn Gamma x A -> A' = (f A) -> atn (mmap f Gamma) x A'.
Proof. induction 1; intros; subst; constructor; eauto. Qed.
Lemma mmap_get {f : term -> term} {Gamma x A'} :
get (mmap f Gamma) x = Some A' -> exists A, A' = (f A) /\ get Gamma x = Some A.
Proof.
intros H. apply get_atn in H. destruct (mmap_atn H) as [A [EA H']].
exists A; eauto using atn_get.
Qed.
Lemma get_mmap {f : term -> term} {Gamma x A A'} :
get Gamma x = Some A -> A' = (f A) -> get (mmap f Gamma) x = Some A'.
Proof. intros. apply atn_get. apply get_atn in H. eapply atn_mmap; eauto. Qed.
Lemma mmap_get_None {f : term -> term} {Gamma x} :
get (mmap f Gamma) x = None -> get Gamma x = None.
Proof.
intros H. case_eq (get Gamma x); trivial. intros t Et. exfalso.
eapply @get_mmap with (f:=f) in Et; eauto. congruence.
Qed.
Lemma get_mmap_None {f : term -> term} {Gamma x} :
get Gamma x = None -> get (mmap f Gamma) x = None.
Proof.
intros H. case_eq (get (mmap f Gamma) x); trivial. intros t Et. exfalso.
destruct (mmap_get Et) as [s [_ H']]. congruence.
Qed.
(* dependent context lookup *)
Inductive atnd: list term -> var -> term -> Prop :=
| Atnd0 Delta A A' :
A' = A.[ren(+1)] -> atnd (A :: Delta) 0 A'
| AtndS Delta x A B B' :
atnd Delta x B -> B' = B.[ren(+1)] -> atnd (A :: Delta) (S x) B'.
Fixpoint getD (Gamma : list term) n : option term :=
match Gamma with
| nil => fun n => None
| s :: Gamma => Some s.[ren(+1)] .: getD Gamma >>> fmap(subst(ren(+1)))
end n.
Arguments getD !Gamma/ n.
Lemma getD_atnd Gamma n s : getD Gamma n = Some s -> atnd Gamma n s.
Proof.
revert n s. induction Gamma; intros n s E.
- inversion E.
- destruct n as [|n].
+ simpl in E. inversion E; subst. now constructor.
+ simpl in E. case_eq (getD Gamma n); [intros t E'|intros E']; rewrite E' in E; inversion E; subst.
econstructor; eauto.
Qed.
Lemma atnd_getD Gamma n s : atnd Gamma n s -> getD Gamma n = Some s.
Proof. induction 1; intros; subst; simpl; now autorew. Qed.
(* Connecting the two notions *)
Lemma getD_get Gamma n : getD Gamma n = subst (ren(+S n)) <$> (get Gamma n).
Proof.
revert Gamma; induction n; intros; destruct Gamma; simpl; autorew; trivial.
asimpl. autodestr. autosubst.
Qed.
Lemma getD_cons (s : term) (Gamma : list term) :
getD (s :: Gamma) = (Some s.[ren (+1)]) .: getD Gamma..[ren (+1)].
Proof.
f_ext. intros [|n]; trivial. rewrite getD_get.
replace ((Some s.[ren (+1)] .: getD Gamma..[ren (+1)]) (S n)) with (getD Gamma..[ren (+1)] n) by reflexivity.
repeat rewrite getD_get. asimpl.
case_eq (get Gamma n).
- intros t Et.
assert (E: get Gamma..[ren (+1)] n = Some t.[ren (+1)]) by (eapply get_mmap; eauto).
rewrite E; autosubst.
- intros E. rewrite get_mmap_None; trivial.
Qed.
End SubstInstance.
(* Generic context renamings *)
Section ContextRenamings.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}
{Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}.
Definition cr xi Gamma Delta := forall n t, atnd Gamma n t -> atnd Delta (xi n) t.[ren xi].
Lemma cr_up t xi Gamma Delta : cr xi Gamma Delta -> cr (upren xi) (t :: Gamma) (t.[ren xi] :: Delta).
Proof. intros c [|] s l; inversion l; subst; econstructor; eauto; autosubst. Qed.
Lemma cr_shift Gamma t : cr (+1) Gamma (t :: Gamma).
Proof. intros n s l. asimpl. econstructor; eauto. Qed.
End ContextRenamings.
Section CtxBoolFun.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}.
Definition bfr (xi : var -> var) delta gamma := forall n, gamma n = true -> delta (xi n) = true.
Lemma bfr_up b xi delta gamma : bfr xi delta gamma -> bfr (upren xi) (b .: delta) (b .: gamma).
Proof. intros H [|n] e; asimpl; eauto. Qed.
Lemma bfr_shift b gamma : bfr (+1) (b .: gamma) gamma.
Proof. intros n e. trivial. Qed.
Lemma bfr_ushift gamma : bfr (-1) gamma (false .: gamma).
Proof. intros [|n]; asimpl; trivial. discriminate. Qed.
End CtxBoolFun.
Section Coincidence.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}
{Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}.
Definition subst_coinc (gamma : var -> bool) (sigma tau : var -> term) := forall n, gamma n = true -> sigma n = tau n.
Lemma subst_coinc_id gamma sigma : subst_coinc gamma sigma sigma.
Proof. now intros n. Qed.
Lemma subst_coinc_up b gamma sigma tau : subst_coinc gamma sigma tau -> subst_coinc (b .: gamma) (up sigma) (up tau).
Proof. intros H [|n] A; asimpl in *; trivial. now rewrite H. Qed.
(* Lemma ren_coinc_hd_f b gamma xi zeta : b = false -> subst_coinc gamma (ren xi) tau -> subst_coinc (b .: gamma) (ren (x .: xi)) (ren (z .: zeta)). *)
(* Proof. intros E H |n A; asimpl in *; try congruence. now apply H. Qed. *)
Lemma subst_coinc_hd_f b gamma sigma tau : b = false -> subst_coinc gamma ((+1) >>> sigma) ((+1) >>> tau) -> subst_coinc (b .: gamma) sigma tau.
Proof. intros E H [|n] A; asimpl in *; try congruence. now apply (H n). Qed.
End Coincidence.
Section CoincidenceHSubst.
Context {type : Type}.
Context {Ids_type : Ids type} {Rename_type : Rename type}
{Subst_type : Subst type} {SubstLemmas_type : SubstLemmas type}.
Context {term : Type}.
Context {Ids_term : Ids term} {Rename_term : Rename term}
{Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}
{HSubst_term : HSubst type term} {HSubstLemmas_term : HSubstLemmas type term}.
Lemma subst_coinc_hcomp gamma sigma tau rho : subst_coinc gamma sigma tau -> subst_coinc gamma (sigma >>| rho) (tau >>| rho).
Proof. intros H n E. asimpl. f_equal. eauto. Qed.
End CoincidenceHSubst.