+Inductive CoreCoercion : Type :=
+ CoreCoercionRefl : CoreType -> CoreCoercion
+ | CoreCoercionTyConAppCo : CoreTyCon -> list CoreCoercion -> CoreCoercion
+ | CoreCoercionAppCo : CoreCoercion -> CoreCoercion -> CoreCoercion
+ | CoreCoercionForAllCo : CoreVar -> CoreCoercion -> CoreCoercion
+ | CoreCoercionCoVarCo : CoreVar -> CoreCoercion
+ | CoreCoercionAxiomInstCo : CoreCoercionCoAxiom -> list CoreCoercion -> CoreCoercion
+ | CoreCoercionUnsafeCo : CoreType -> CoreType -> CoreCoercion
+ | CoreCoercionSymCo : CoreCoercion -> CoreCoercion
+ | CoreCoercionTransCo : CoreCoercion -> CoreCoercion -> CoreCoercion
+ | CoreCoercionNthCo : Int -> CoreCoercion -> CoreCoercion
+ | CoreCoercionInstCo : CoreCoercion -> CoreType -> CoreCoercion.
+
+Extract Inductive CoreCoercion =>
+ "Coercion.Coercion" [
+ "Coercion.Refl"
+ "Coercion.TyConAppCo"
+ "Coercion.AppCo"
+ "Coercion.ForAllCo"
+ "Coercion.CoVarCo"
+ "Coercion.AxiomInstCo"
+ "Coercion.UnsafeCo"
+ "Coercion.SymCo"
+ "Coercion.TransCo"
+ "Coercion.NthCo"
+ "Coercion.InstCo" ].
+