cpr G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
| cpr_zeta : ∀G,L,V,T1,T,T2. cpr G (L.ⓓV) T1 T →
⇧[0, 1] T2 ≡ T → cpr G L (+ⓓV.T1) T2
cpr G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
| cpr_zeta : ∀G,L,V,T1,T,T2. cpr G (L.ⓓV) T1 T →
⇧[0, 1] T2 ≡ T → cpr G L (+ⓓV.T1) T2
-| cpr_tau : ∀G,L,V,T1,T2. cpr G L T1 T2 → cpr G L (ⓝV.T1) T2
+| cpr_eps : ∀G,L,V,T1,T2. cpr G L T1 T2 → cpr G L (ⓝV.T1) T2
| cpr_beta : ∀a,G,L,V1,V2,W1,W2,T1,T2.
cpr G L V1 V2 → cpr G L W1 W2 → cpr G (L.ⓛW1) T1 T2 →
cpr G L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2)
| cpr_beta : ∀a,G,L,V1,V2,W1,W2,T1,T2.
cpr G L V1 V2 → cpr G L W1 W2 → cpr G (L.ⓛW1) T1 T2 →
cpr G L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2)
elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -L1 *
/3 width=6 by cpr_delta/
|3,7: /4 width=1 by lsubr_bind, cpr_bind, cpr_beta/
elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -L1 *
/3 width=6 by cpr_delta/
|3,7: /4 width=1 by lsubr_bind, cpr_bind, cpr_beta/
|5,8: /4 width=3 by lsubr_bind, cpr_zeta, cpr_theta/
]
qed-.
|5,8: /4 width=3 by lsubr_bind, cpr_zeta, cpr_theta/
]
qed-.