yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add tstar to preserve eta normal forms

Browse source
This commit is contained in:
Yiyun Liu 2025-01-27 16:44:48 -05:00
parent 11d23afa45
commit 9f80013df6
3 changed files with 209 additions and 81 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
syntax.sig
View file

@ -9,7 +9,7 @@ Void : Ty
PL : PTag
PR : PTag
PAbs : Ty -> (bind PTm in PTm) -> PTm
PAbs : (bind PTm in PTm) -> PTm
PApp : PTm -> PTm -> PTm
PPair : PTm -> PTm -> PTm
PProj : PTag -> PTm -> PTm

110
theories/Autosubst2/syntax.v
View file

@ -19,43 +19,17 @@ Proof.
exact (eq_refl).
Qed.
Inductive Ty : Type :=
| Fun : Ty -> Ty -> Ty
| Prod : Ty -> Ty -> Ty
| Void : Ty.
Lemma congr_Fun {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Fun s0 s1 = Fun t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Fun x s1) H0))
(ap (fun x => Fun t0 x) H1)).
Qed.
Lemma congr_Prod {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Prod s0 s1 = Prod t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Prod x s1) H0))
(ap (fun x => Prod t0 x) H1)).
Qed.
Lemma congr_Void : Void = Void.
Proof.
exact (eq_refl).
Qed.
Inductive PTm (n_PTm : nat) : Type :=
| VarPTm : fin n_PTm -> PTm n_PTm
| PAbs : Ty -> PTm (S n_PTm) -> PTm n_PTm
| PAbs : PTm (S n_PTm) -> PTm n_PTm
| PApp : PTm n_PTm -> PTm n_PTm -> PTm n_PTm
| PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm
| PProj : PTag -> PTm n_PTm -> PTm n_PTm.
Lemma congr_PAbs {m_PTm : nat} {s0 : Ty} {s1 : PTm (S m_PTm)} {t0 : Ty}
{t1 : PTm (S m_PTm)} (H0 : s0 = t0) (H1 : s1 = t1) :
PAbs m_PTm s0 s1 = PAbs m_PTm t0 t1.
Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_PTm)}
(H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => PAbs m_PTm x s1) H0))
(ap (fun x => PAbs m_PTm t0 x) H1)).
exact (eq_trans eq_refl (ap (fun x => PAbs m_PTm x) H0)).
Qed.
Lemma congr_PApp {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm}
@ -98,7 +72,7 @@ Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat}
(xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm :=
match s with
| VarPTm _ s0 => VarPTm n_PTm (xi_PTm s0)
| PAbs _ s0 s1 => PAbs n_PTm s0 (ren_PTm (upRen_PTm_PTm xi_PTm) s1)
| PAbs _ s0 => PAbs n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0)
| PApp _ s0 s1 => PApp n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
| PPair _ s0 s1 => PPair n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
| PProj _ s0 s1 => PProj n_PTm s0 (ren_PTm xi_PTm s1)
@ -122,7 +96,7 @@ Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat}
:=
match s with
| VarPTm _ s0 => sigma_PTm s0
| PAbs _ s0 s1 => PAbs n_PTm s0 (subst_PTm (up_PTm_PTm sigma_PTm) s1)
| PAbs _ s0 => PAbs n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0)
| PApp _ s0 s1 =>
PApp n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
| PPair _ s0 s1 =>
@ -155,9 +129,9 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm)
: subst_PTm sigma_PTm s = s :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s1)
| PAbs _ s0 =>
congr_PAbs
(idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0)
| PApp _ s0 s1 =>
congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0)
(idSubst_PTm sigma_PTm Eq_PTm s1)
@ -194,10 +168,10 @@ Fixpoint extRen_PTm {m_PTm : nat} {n_PTm : nat}
ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
match s with
| VarPTm _ s0 => ap (VarPTm n_PTm) (Eq_PTm s0)
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
| PAbs _ s0 =>
congr_PAbs
(extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
(upExtRen_PTm_PTm _ _ Eq_PTm) s1)
(upExtRen_PTm_PTm _ _ Eq_PTm) s0)
| PApp _ s0 s1 =>
congr_PApp (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
(extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
@ -235,10 +209,10 @@ Fixpoint ext_PTm {m_PTm : nat} {n_PTm : nat}
subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
| PAbs _ s0 =>
congr_PAbs
(ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
(upExt_PTm_PTm _ _ Eq_PTm) s1)
(upExt_PTm_PTm _ _ Eq_PTm) s0)
| PApp _ s0 s1 =>
congr_PApp (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
(ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
@ -275,10 +249,10 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
{struct s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s :=
match s with
| VarPTm _ s0 => ap (VarPTm l_PTm) (Eq_PTm s0)
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
| PAbs _ s0 =>
congr_PAbs
(compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
(upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s1)
(upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0)
| PApp _ s0 s1 =>
congr_PApp (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0)
(compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
@ -325,10 +299,10 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
{struct s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
| PAbs _ s0 =>
congr_PAbs
(compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm)
(up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s1)
(up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0)
| PApp _ s0 s1 =>
congr_PApp (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0)
(compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
@ -395,10 +369,10 @@ Fixpoint compSubstRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
| PAbs _ s0 =>
congr_PAbs
(compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm)
(up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s1)
(up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0)
| PApp _ s0 s1 =>
congr_PApp (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0)
(compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
@ -467,10 +441,10 @@ Fixpoint compSubstSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
| PAbs _ s0 =>
congr_PAbs
(compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
(up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s1)
(up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0)
| PApp _ s0 s1 =>
congr_PApp (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0)
(compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
@ -580,10 +554,10 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat}
(s : PTm m_PTm) {struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
| PAbs _ s0 =>
congr_PAbs
(rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
(rinstInst_up_PTm_PTm _ _ Eq_PTm) s1)
(rinstInst_up_PTm_PTm _ _ Eq_PTm) s0)
| PApp _ s0 s1 =>
congr_PApp (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0)
(rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
@ -663,6 +637,30 @@ Proof.
exact (fun x => eq_refl).
Qed.
Inductive Ty : Type :=
| Fun : Ty -> Ty -> Ty
| Prod : Ty -> Ty -> Ty
| Void : Ty.
Lemma congr_Fun {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Fun s0 s1 = Fun t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Fun x s1) H0))
(ap (fun x => Fun t0 x) H1)).
Qed.
Lemma congr_Prod {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Prod s0 s1 = Prod t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Prod x s1) H0))
(ap (fun x => Prod t0 x) H1)).
Qed.
Lemma congr_Void : Void = Void.
Proof.
exact (eq_refl).
Qed.
Class Up_PTm X Y :=
up_PTm : X -> Y.

178
theories/fp_red.v
View file

@ -22,16 +22,17 @@ Ltac spec_refl := ltac2:(spec_refl ()).
Module ERed.
Inductive R {n} : PTm n -> PTm n -> Prop :=
(****************** Eta ***********************)
| AppEta A a0 a1 :
| AppEta a0 a1 :
R a0 a1 ->
R (PAbs A (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1
| PairEta a0 a1 :
R (PAbs (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1
| PairEta a0 b0 a1 :
R a0 a1 ->
R (PPair (PProj PL a0) (PProj PR a0)) a1
R b0 a1 ->
R (PPair (PProj PL a0) (PProj PR b0)) a1
(*************** Congruence ********************)
| AbsCong A a0 a1 :
| AbsCong a0 a1 :
R a0 a1 ->
R (PAbs A a0) (PAbs A a1)
R (PAbs a0) (PAbs a1)
| AppCong a0 a1 b0 b1 :
R a0 a1 ->
R b0 b1 ->
@ -53,8 +54,8 @@ Module ERed.
Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
Lemma AppEta' n A a0 a1 (u : PTm n) :
u = (PAbs A (PApp (ren_PTm shift a0) (VarPTm var_zero))) ->
Lemma AppEta' n a0 a1 (u : PTm n) :
u = (PAbs (PApp (ren_PTm shift a0) (VarPTm var_zero))) ->
R a0 a1 ->
R u a1.
Proof. move => ->. apply AppEta. Qed.
@ -65,8 +66,8 @@ Module ERed.
move => h. move : m ξ.
elim : n a b /h.
move => n A a0 a1 ha iha m ξ /=.
eapply AppEta' with (A := A); eauto. by asimpl.
move => n a0 a1 ha iha m ξ /=.
eapply AppEta'; eauto. by asimpl.
all : qauto ctrs:R.
Qed.
@ -91,8 +92,8 @@ Module ERed.
R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b).
Proof.
move => + h. move : m ρ0 ρ1. elim : n a b / h => n.
move => A a0 a1 ha iha m ρ0 ρ1 hρ /=.
eapply AppEta' with (A := A); eauto. by asimpl.
move => a0 a1 ha iha m ρ0 ρ1 hρ /=.
eapply AppEta'; eauto. by asimpl.
all : hauto lq:on ctrs:R use:morphing_up.
Qed.
@ -120,9 +121,9 @@ with SN {n} : PTm n -> Prop :=
SN a ->
SN b ->
SN (PPair a b)
| N_Abs A a :
| N_Abs a :
SN a ->
SN (PAbs A a)
SN (PAbs a)
| N_SNe a :
SNe a ->
SN a
@ -131,9 +132,9 @@ with SN {n} : PTm n -> Prop :=
SN b ->
SN a
with TRedSN {n} : PTm n -> PTm n -> Prop :=
| N_β A a b :
| N_β a b :
SN b ->
TRedSN (PApp (PAbs A a) b) (subst_PTm (scons b VarPTm) a)
TRedSN (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a)
| N_AppL a0 a1 b :
TRedSN a0 a1 ->
TRedSN (PApp a0 b) (PApp a1 b)
@ -153,6 +154,27 @@ Scheme sne_ind := Induction for SNe Sort Prop
Combined Scheme sn_mutual from sne_ind, sn_ind, sred_ind.
Fixpoint ne {n} (a : PTm n) :=
match a with
| VarPTm i => true
| PApp a b => ne a && nf b
| PAbs a => false
| PPair _ _ => false
| PProj _ a => ne a
end
with nf {n} (a : PTm n) :=
match a with
| VarPTm i => true
| PApp a b => ne a && nf b
| PAbs a => nf a
| PPair a b => nf a && nf b
| PProj _ a => ne a
end.
Lemma ne_nf n a : @ne n a -> nf a.
Proof. elim : a => //=. Qed.
Inductive TRedSN' {n} (a : PTm n) : PTm n -> Prop :=
| T_Refl :
TRedSN' a a
@ -182,7 +204,7 @@ Proof.
+ have /iha : (ERed.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
sfirstorder use:SN_Proj.
+ sauto lq:on.
- move => A a ha iha b.
- move => a ha iha b.
inversion 1; subst.
+ have : ERed.R (PApp (ren_PTm shift a0) (VarPTm var_zero)) (PApp (ren_PTm shift b) (VarPTm var_zero)).
apply ERed.AppCong; eauto using ERed.refl.
@ -192,7 +214,7 @@ Proof.
+ sauto lq:on.
- sauto lq:on.
- sauto lq:on.
- move => A a b ha iha c h0.
- move => a b ha iha c h0.
inversion h0; subst.
inversion H1; subst.
+ exists (PApp a1 b1). split. sfirstorder.
@ -208,7 +230,7 @@ Proof.
elim /ERed.inv => //= _.
move => p a0 a1 ha [*]. subst.
elim /ERed.inv : ha => //= _.
+ move => a0 a2 ha [*]. subst.
+ move => a0 b0 a2 ha ha' [*]. subst.
exists (PProj PL a1).
split. sauto.
sauto lq:on.
@ -217,7 +239,7 @@ Proof.
elim /ERed.inv => //=_.
move => p a0 a1 + [*]. subst.
elim /ERed.inv => //=_.
+ move => a0 a2 h [*]. subst.
+ move => a0 b0 a2 h0 h1 [*]. subst.
exists (PProj PR a1).
split. sauto.
sauto lq:on.
@ -228,16 +250,16 @@ Admitted.
Module RRed.
Inductive R {n} : PTm n -> PTm n -> Prop :=
(****************** Eta ***********************)
| AppAbs A a b :
R (PApp (PAbs A a) b) (subst_PTm (scons b VarPTm) a)
| AppAbs a b :
R (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a)
| ProjPair p a b :
R (PProj p (PPair a b)) (if p is PL then a else b)
(*************** Congruence ********************)
| AbsCong A a0 a1 :
| AbsCong a0 a1 :
R a0 a1 ->
R (PAbs A a0) (PAbs A a1)
R (PAbs a0) (PAbs a1)
| AppCong0 a0 a1 b :
R a0 a1 ->
R (PApp a0 b) (PApp a1 b)
@ -255,4 +277,112 @@ Module RRed.
R (PProj p a0) (PProj p a1).
Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b.
Proof.
move E : (ren_PTm ξ a) => u h.
move : n ξ a E. elim : m u b/h.
- move => n a b m ξ []//=. move => []//= t t0 [*]. subst.
eexists. split. apply AppAbs. by asimpl.
- move => n p a b m ξ []//=.
move => p0 []//=. hauto q:on ctrs:R.
- move => n a0 a1 ha iha m ξ []//=.
move => p [*]. subst.
spec_refl.
move : iha => [t [h0 h1]]. subst.
eexists. split. eauto using AbsCong.
by asimpl.
- move => n a0 a1 b ha iha m ξ []//=.
hauto lq:on ctrs:R.
- move => n a b0 b1 h ih m ξ []//=.
hauto lq:on ctrs:R.
- move => n a0 a1 b ha iha m ξ []//=.
hauto lq:on ctrs:R.
- move => n a b0 b1 h ih m ξ []//=.
hauto lq:on ctrs:R.
- move => n p a0 a1 ha iha m ξ []//=.
hauto lq:on ctrs:R.
Qed.
End RRed.
Function tstar {n} (a : PTm n) :=
match a with
| VarPTm i => a
| PAbs a => PAbs (tstar a)
| PApp (PAbs a) b => subst_PTm (scons (tstar b) VarPTm) (tstar a)
| PApp a b => PApp (tstar a) (tstar b)
| PPair a b => PPair (tstar a) (tstar b)
| PProj p (PPair a b) => if p is PL then (tstar a) else (tstar b)
| PProj p a => PProj p (tstar a)
end.
Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b ->
ERed.R c b.
Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b -> RRed.R a c ->
ERed.R c b.
Proof.
move => h. move : c.
elim : n a b /h=>//=n.
- move => a0 a1 ha iha u hu.
elim /RRed.inv => //= _.
move => a2 a3 h [*]. subst.
elim / RRed.inv : h => //_.
+ move => a2 b0 [h0 h1 h2]. subst.
case : a0 h0 ha iha =>//=.
move => u [?] ha iha. subst.
by asimpl.
+ move => a2 b4 b0 h [*]. subst.
move /RRed.antirenaming : h.
hauto lq:on ctrs:ERed.R.
+ move => a2 b0 b1 h [*]. subst.
inversion h.
- move => a0 b0 a1 ha iha hb ihb u hu.
elim /RRed.inv => //=_.
+ move => a2 a3 b1 h0 [*]. subst.
elim /RRed.inv : h0 => //=_.
* move => p a2 b1 [*]. subst.
elim /ERed.inv : ha => //=_.
** sauto lq:on.
** move => a0 a2 b2 b3 h h' [*]. subst.
Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b -> RRed.R a c ->
ERed.R a c.
Proof.
move => h. move : c.
elim : n a b /h=>//=.
- move => n A a0 a1 ha iha c ha1.
elim /RRed.inv => //=_.
move => A0 a2 a3 hr [*]. subst.
set u := a0 in hr *.
set q := a3 in hr *.
elim / RRed.inv : hr => //_.
+ move => A0 a2 b0 [h0] h1 h2. subst.
subst u q.
rewrite h0. apply ERed.AppEta.
subst.
case : a0 ha iha h0 => //= B a ha iha [*]. subst.
asimpl.
admit.
+ subst u q.
move => a2 a4 b0 hr [*]. subst.
move /RRed.antirenaming : hr => [b0 [h0 h1]]. subst.
hauto lq:on ctrs:ERed.R use:ERed.renaming.
+ subst u q.
move => a2 b0 b1 h [*]. subst.
inversion h.
- move => n a0 a1 ha iha v hv.
elim /RRed.inv => //=_.
+ move => a2 a3 b0 h [*]. subst.
elim /RRed.inv : h => //=_.
* move => p a2 b0 [*]. subst.
elim /ERed.inv : ha=>//= _.
move => a0 a2 h [*]. subst.
best.
apply ERed.PairEta.
-