- | RAppT Γ Δ Σ κ σ τ p y => let case_RAppT := tt in _
- | RAppCo Γ Δ Σ κ σ₁ σ₂ σ γ p => let case_RAppCo := tt in _
- | RAbsCo Γ Δ Σ κ σ cc σ₁ σ₂ p y => let case_RAbsCo := tt in _
+ | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
+ | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
+ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _