- ujudg2exprType ξ (Γ >> Δ > h |- t) ->
- ujudg2exprType ξ (Γ >> Δ > j |- t) :=
- match r as R in Arrange H C return ujudg2exprType ξ (Γ >> Δ > H |- t) ->
- ujudg2exprType ξ (Γ >> Δ > C |- t) with
+ ujudg2exprType Γ ξ Δ h t ->
+ ujudg2exprType Γ ξ Δ j t :=
+ match r as R in Arrange H C return
+ ujudg2exprType Γ ξ Δ H t ->
+ ujudg2exprType Γ ξ Δ C t
+ with