Variable R : Type.

Fail Inductive I : R := c : R.