diff --git a/liquid-prelude.cabal b/liquid-prelude.cabal
--- a/liquid-prelude.cabal
+++ b/liquid-prelude.cabal
@@ -1,6 +1,6 @@
 cabal-version:      1.24
 name:               liquid-prelude
-version:            0.9.10.1.2
+version:            0.9.12.2.1
 synopsis:           General utility modules for LiquidHaskell
 description:        General utility modules for LiquidHaskell.
 license:            BSD3
@@ -30,5 +30,5 @@
                     , ghc-prim
                     , bytestring           >= 0.10.12.1
                     , containers           >= 0.6.4.1
-                    , liquidhaskell        >= 0.9.10.1.2
+                    , liquidhaskell        >= 0.9.12.2.1
   default-language:   Haskell2010
diff --git a/src/Language/Haskell/Liquid/ProofCombinators.hs b/src/Language/Haskell/Liquid/ProofCombinators.hs
--- a/src/Language/Haskell/Liquid/ProofCombinators.hs
+++ b/src/Language/Haskell/Liquid/ProofCombinators.hs
@@ -183,6 +183,10 @@
 {-@ measure prop :: a -> b           @-}
 {-@ type Prop E = {v:_ | prop v = E} @-}
 
+-- New syntax for "inductive propositions", aka indexed types, it
+-- should be used in place of `Prop` that is kept for backward
+-- compatibility.
+{-@ type Ix typ E = {v:typ | prop v = E} @-}
 
 -------------------------------------------------------------------------------
 -- PLE-specific