diff --git a/meta/src/main/java/org/arend/lib/meta/ExtMeta.java b/meta/src/main/java/org/arend/lib/meta/ExtMeta.java
index 0b415b2c..bd45dfe4 100644
--- a/meta/src/main/java/org/arend/lib/meta/ExtMeta.java
+++ b/meta/src/main/java/org/arend/lib/meta/ExtMeta.java
@@ -159,7 +159,7 @@ private TypedExpression hidingIRef(ConcreteExpression expr, CoreExpression type)
       return binding == null ? typechecker.typecheck(expr, type) : checkGoals(typechecker.withFreeBindings(new FreeBindingsModifier().remove(binding), tc -> tc.typecheck(expr, type)));
     }
 
-    private ConcreteExpression makeCoeLambda(CoreParameter typeParams, CoreBinding paramBinding, Set<CoreBinding> used, Map<CoreBinding, PathExpression> sigmaRefs, ConcreteFactory factory) {
+    private ConcreteExpression makeCoeLambda(CoreParameter typeParams, CoreBinding paramBinding, CoreExpression paramType, Set<CoreBinding> used, Map<CoreBinding, PathExpression> sigmaRefs, ConcreteFactory factory) {
       ArendRef coeRef = factory.local("i");
       return factory.lam(Collections.singletonList(factory.param(coeRef)), factory.meta("ext_coe", new MetaDefinition() {
         @Override
@@ -170,7 +170,7 @@ private ConcreteExpression makeCoeLambda(CoreParameter typeParams, CoreBinding p
               substitution.add(new SubstitutionPair(param.getBinding(), sigmaRefs.get(param.getBinding()).applyAt(coeRef, factory, ext)));
             }
           }
-          CoreExpression result = typechecker.substitute(paramBinding.getTypeExpr().normalize(NormalizationMode.WHNF), LevelSubstitution.EMPTY, substitution);
+          CoreExpression result = typechecker.substitute((paramType == null ? paramBinding.getTypeExpr() : paramType).normalize(NormalizationMode.WHNF), LevelSubstitution.EMPTY, substitution);
           return result == null ? null : result.computeTyped(true);
         }
       }));
@@ -239,12 +239,15 @@ private ConcreteExpression generate(ConcreteExpression arg, CoreExpression type,
         }
 
         Set<CoreClassField> propFields = new HashSet<>();
-        Set<CoreBinding> propBindings = new HashSet<>();
+        Map<CoreBinding, CoreExpression> propBindings = new HashMap<>();
         int i = 0;
         for (CoreParameter param = typeParams; param.hasNext(); param = param.getNext(), i++) {
-          boolean isProp = classFields != null && classFields.get(i).isProperty() || Utils.isProp(param.getTypeExpr());
-          if (isProp) {
-            propBindings.add(param.getBinding());
+          CoreExpression propType = classFields != null && classFields.get(i).isProperty() ? param.getTypeExpr() : null;
+          if (propType == null) {
+            propType = Utils.minimizeToProp(param.getTypeExpr());
+          }
+          if (propType != null) {
+            propBindings.put(param.getBinding(), propType);
             if (classFields != null) {
               propFields.add(classFields.get(i));
             }
@@ -353,7 +356,7 @@ private ConcreteExpression generate(ConcreteExpression arg, CoreExpression type,
         for (CoreParameter param = typeParams; param.hasNext(); param = param.getNext(), i++) {
           Set<CoreBinding> used = new HashSet<>();
           CoreBinding paramBinding = param.getBinding();
-          boolean isProp = propBindings.contains(paramBinding);
+          boolean isProp = propBindings.containsKey(paramBinding);
           if (!bindings.isEmpty()) {
             if (param.getTypeExpr().processSubexpression(e -> {
               if (!(e instanceof CoreReferenceExpression)) {
@@ -362,7 +365,7 @@ private ConcreteExpression generate(ConcreteExpression arg, CoreExpression type,
               CoreBinding binding = ((CoreReferenceExpression) e).getBinding();
               if (bindings.contains(binding)) {
                 if (!isProp) {
-                  if (propBindings.contains(binding)) {
+                  if (propBindings.containsKey(binding)) {
                     typechecker.getErrorReporter().report(new TypecheckingError("Non-propositional fields cannot depend on propositional ones", marker));
                     return CoreExpression.FindAction.STOP;
                   }
@@ -453,7 +456,7 @@ private ConcreteExpression generate(ConcreteExpression arg, CoreExpression type,
               CoreBinding binding = used.size() > 1 ? null : used.iterator().next();
               PathExpression pathExpr = binding == null ? null : sigmaRefs.get(binding);
               if (pathExpr == null || !pathExpr.getClass().equals(PathExpression.class)) {
-                leftExpr = factory.app(factory.ref(ext.prelude.getCoerce().getRef()), true, Arrays.asList(makeCoeLambda(typeParams, paramBinding, used, sigmaRefs, factory), leftExpr, factory.ref(ext.prelude.getRight().getRef())));
+                leftExpr = factory.app(factory.ref(ext.prelude.getCoerce().getRef()), true, Arrays.asList(makeCoeLambda(typeParams, paramBinding, propBindings.get(paramBinding), used, sigmaRefs, factory), leftExpr, factory.ref(ext.prelude.getRight().getRef())));
               } else {
                 leftExpr = factory.app(factory.ref(ext.transport.getRef()), true, Arrays.asList(SubstitutionMeta.makeLambda(paramBinding.getTypeExpr(), binding, factory), pathExpr.pathExpression, leftExpr));
               }
@@ -588,8 +591,8 @@ public void solve(@NotNull ExpressionTypechecker typechecker, @NotNull ConcreteG
             ArendRef pRef = factory.local("i");
             field = applyPath(pRef, pathExpr.applyAt(pRef, factory, ext));
             useLet = false;
-          } else if (propBindings.contains(paramBinding)) {
-            field = factory.app(factory.ref(ext.propDPI.getRef()), true, Arrays.asList(makeCoeLambda(typeParams, paramBinding, usedList.get(i), fieldsMap, factory), makeProj(factory, left, i, classFields), makeProj(factory, right, i, classFields)));
+          } else if (propBindings.containsKey(paramBinding)) {
+            field = factory.app(factory.ref(ext.propDPI.getRef()), true, Arrays.asList(makeCoeLambda(typeParams, paramBinding, propBindings.get(paramBinding), usedList.get(i), fieldsMap, factory), makeProj(factory, left, i, classFields), makeProj(factory, right, i, classFields)));
             useLet = true;
           } else {
             boolean isDependent = dependentBindings.contains(paramBinding);
@@ -664,7 +667,7 @@ public void solve(@NotNull ExpressionTypechecker typechecker, @NotNull ConcreteG
               }
             }
 
-            field = isDependent ? factory.appBuilder(factory.ref(ext.pathOver.getRef())).app(makeCoeLambda(typeParams, paramBinding, usedList.get(i), fieldsMap, factory), false).app(proj).build() : proj;
+            field = isDependent ? factory.appBuilder(factory.ref(ext.pathOver.getRef())).app(makeCoeLambda(typeParams, paramBinding, propBindings.get(paramBinding), usedList.get(i), fieldsMap, factory), false).app(proj).build() : proj;
             i1++;
           }
 
diff --git a/meta/src/main/java/org/arend/lib/util/Utils.java b/meta/src/main/java/org/arend/lib/util/Utils.java
index fec26213..4c254bcb 100644
--- a/meta/src/main/java/org/arend/lib/util/Utils.java
+++ b/meta/src/main/java/org/arend/lib/util/Utils.java
@@ -306,10 +306,16 @@ public static boolean safeCompare(ExpressionTypechecker typechecker, UncheckedEx
   }
 
   public static boolean isProp(CoreExpression type) {
-    CoreExpression typeType = type.normalize(NormalizationMode.WHNF).computeType(true).normalize(NormalizationMode.WHNF);
+    CoreExpression typeType = type.normalize(NormalizationMode.WHNF).computeType().normalize(NormalizationMode.WHNF);
     return typeType instanceof CoreUniverseExpression && ((CoreUniverseExpression) typeType).getSort().isProp();
   }
 
+  public static CoreExpression minimizeToProp(CoreExpression type) {
+    type = type.normalize(NormalizationMode.WHNF).minimizeLevels();
+    CoreExpression typeType = type.computeType().normalize(NormalizationMode.WHNF);
+    return typeType instanceof CoreUniverseExpression && ((CoreUniverseExpression) typeType).getSort().isProp() ? type : null;
+  }
+
   public static List<CoreClassField> getNotImplementedField(CoreClassCallExpression classCall) {
     List<CoreClassField> classFields = new ArrayList<>();
     for (CoreClassField field : classCall.getDefinition().getNotImplementedFields()) {
diff --git a/src/Algebra/Ring/Poly.ard b/src/Algebra/Ring/Poly.ard
index 2e3b4751..4de7c80e 100644
--- a/src/Algebra/Ring/Poly.ard
+++ b/src/Algebra/Ring/Poly.ard
@@ -80,8 +80,8 @@
       | :: a l, padd p e => \lam s => pmap2 padd (gfunc l p (qadd_cons s).2) (qadd_cons {_} {e} {a} {toQPoly p} {l} s).1
       | :: a l, peq => pathOver $ coe_pi *> ext (\lam s => coe_path (path peq) _ idp *> pmap (inv (path peq) *>) (pmap2 (\lam x => pmap2 padd (gfunc l pzero x)) prop-pi set-pi))
 
-    \func toQPoly-equiv {R : AddPointed} : Equiv (toQPoly {R})
-      => contrFibers=>Equiv $ \case \elim __ \with {
+    \lemma toQPoly-equiv {R : AddPointed} : Equiv (toQPoly {R})
+      => contrFibers=>Equiv \case \elim __ \with {
         | in~ l => \new Contr {
           | center => (fromArray l, cfunc l)
           | contraction t => ext (inv (gfunc l t.1 t.2))