| crx_appl_sn: ∀L,V,T. crx h g G L V → crx h g G L (ⓐV.T)
| crx_appl_dx: ∀L,V,T. crx h g G L T → crx h g G L (ⓐV.T)
| crx_ri2 : ∀I,L,V,T. ri2 I → crx h g G L (②{I}V.T)
| crx_appl_sn: ∀L,V,T. crx h g G L V → crx h g G L (ⓐV.T)
| crx_appl_dx: ∀L,V,T. crx h g G L T → crx h g G L (ⓐV.T)
| crx_ri2 : ∀I,L,V,T. ri2 I → crx h g G L (②{I}V.T)