+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "prop2" (instance 3) = "prop21".
+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "prop2" (instance 3) = "prop21".
+
+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "prop2" (instance 3) = "prop21".
+(*napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#))); *)
+
+(* OK *)
+napply (.= (Sig ? ? (?) ?? E (λw,H.
+ (prop11 ?(unary_morphism1_setoid1 ??)???
+ (prop11 ?(unary_morphism1_setoid1 ??)???
+ H
+ ?? (refl ???))
+ ?? (refl1 ???))))).
+napply refl1.
+
+ (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ????
+ (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ????
+ H
+ (refl ??))
+ (refl ? True))))).
+
+prop11 ???????? (prop11 ???????? H (refl ??)) (refl ??))));
+
+napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#)));
+
+
+napply (.= (Sig ? S (λw,x.?) ?? E (λw,H.(H‡#)‡#)));
+(Ex S (λx.?P x y)) ==?==