+ndefinition pseudo_is_comparable: mcu_type → comparable.
+ #mcu; @ (aux_pseudo_type mcu)
+ ##[ nelim mcu;
+ ##[ ##1,2,3,4: napply (zeroc Freescalepseudo_is_comparable)
+ ##| ##5: napply (zeroc IP2022pseudo_is_comparable) ##]
+ ##| nelim mcu;
+ ##[ ##1,2,3,4: napply (forallc Freescalepseudo_is_comparable)
+ ##| ##5: napply (forallc IP2022pseudo_is_comparable) ##]
+ ##| nelim mcu;
+ ##[ ##1,2,3,4: napply (eqc Freescalepseudo_is_comparable)
+ ##| ##5: napply (eqc IP2022pseudo_is_comparable) ##]
+ ##| nelim mcu;
+ ##[ ##1,2,3,4: napply (eqc_to_eq Freescalepseudo_is_comparable)
+ ##| ##5: napply (eqc_to_eq IP2022pseudo_is_comparable) ##]
+ ##| nelim mcu;
+ ##[ ##1,2,3,4: napply (eq_to_eqc Freescalepseudo_is_comparable)
+ ##| ##5: napply (eq_to_eqc IP2022pseudo_is_comparable) ##]
+ ##| nelim mcu;
+ ##[ ##1,2,3,4: napply (neqc_to_neq Freescalepseudo_is_comparable)
+ ##| ##5: napply (neqc_to_neq IP2022pseudo_is_comparable) ##]
+ ##| nelim mcu;
+ ##[ ##1,2,3,4: napply (neq_to_neqc Freescalepseudo_is_comparable)
+ ##| ##5: napply (neq_to_neqc IP2022pseudo_is_comparable) ##]
+ ##| nelim mcu;
+ ##[ ##1,2,3,4: napply (decidable_c Freescalepseudo_is_comparable)
+ ##| ##5: napply (decidable_c IP2022pseudo_is_comparable) ##]
+ ##| nelim mcu;
+ ##[ ##1,2,3,4: napply (symmetric_eqc Freescalepseudo_is_comparable)
+ ##| ##5: napply (symmetric_eqc IP2022pseudo_is_comparable) ##]
+ ##]
+nqed.
+
+unification hint 0 ≔ M:mcu_type ⊢ carr (pseudo_is_comparable M) ≡ aux_pseudo_type M.
+