1
4

1 回答 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 回答