问问题
55 次
1 回答
1
你可以 inline rewrite
,但它仍然很尴尬:
_*¹_ : ∀ {Γ Γ′ P R} {a : Action Γ} (ρ : Ren Γ Γ′) →
P —[ a ]→ R → ρ * P —[ ρ *ᴬ a ]→ ρ * R
ρ *¹ (ν_ {a = a} E) with suc ρ *ᴬ (sucᴿ *ᴬ a) | suc-comm ρ a | suc ρ *¹ E
... | ._ | refl | E' = ν E'
或者suc ρ *¹ E
先引入再改写:
_*¹_ : ∀ {Γ Γ′ P R} {a : Action Γ} (ρ : Ren Γ Γ′) →
P —[ a ]→ R → ρ * P —[ ρ *ᴬ a ]→ ρ * R
ρ *¹ (ν_ {a = a} E) with suc ρ *¹ E
... | E' rewrite suc-comm ρ a = ν E'
于 2014-07-21T08:29:06.253 回答