-interpretation "prop1" 'prop1 c = (prop1 _____ c).
-interpretation "prop11" 'prop1 c = (prop11 _____ c).
-interpretation "prop12" 'prop1 c = (prop12 _____ c).
-interpretation "prop13" 'prop1 c = (prop13 _____ c).
-interpretation "prop2" 'prop2 l r = (prop2 ________ l r).
-interpretation "prop21" 'prop2 l r = (prop21 ________ l r).
-interpretation "prop22" 'prop2 l r = (prop22 ________ l r).
-interpretation "prop23" 'prop2 l r = (prop23 ________ l r).
-interpretation "refl" 'refl = (refl ___).
-interpretation "refl1" 'refl = (refl1 ___).
-interpretation "refl2" 'refl = (refl2 ___).
-interpretation "refl3" 'refl = (refl3 ___).
-
-definition unary_morphism2_of_unary_morphism1: ∀S,T.unary_morphism1 S T → unary_morphism2 S T.
+interpretation "prop1" 'prop1 c = (prop1 ????? c).
+interpretation "prop11" 'prop1 c = (prop11 ????? c).
+interpretation "prop12" 'prop1 c = (prop12 ????? c).
+interpretation "prop13" 'prop1 c = (prop13 ????? c).
+interpretation "prop2" 'prop2 l r = (prop2 ???????? l r).
+interpretation "prop21" 'prop2 l r = (prop21 ???????? l r).
+interpretation "prop22" 'prop2 l r = (prop22 ???????? l r).
+interpretation "prop23" 'prop2 l r = (prop23 ???????? l r).
+interpretation "refl" 'refl = (refl ???).
+interpretation "refl1" 'refl = (refl1 ???).
+interpretation "refl2" 'refl = (refl2 ???).
+interpretation "refl3" 'refl = (refl3 ???).
+
+definition unary_morphism2_of_unary_morphism1:
+ ∀S,T:setoid1.unary_morphism1 S T → unary_morphism2 (setoid2_of_setoid1 S) T.