-unification hint 0 ≔
- A : setoid, B,C : 𝛀^A;
- R ≟ (mk_ext_powerclass ? (B - C) (ext_prop ? (substract_is_ext ? B C)))
-(*-------------------------------------------------------------------------*) ⊢
- ext_carr A R ≡ substract ? (ext_carr ? B) (ext_carr ? C).
+unification hint 0 ≔ A : setoid, B,C : 𝛀^A;
+ AA ≟ carr A,
+ BB ≟ ext_carr ? B,
+ CC ≟ ext_carr ? C,
+ R ≟ mk_ext_powerclass ?
+ (ext_carr ? B - ext_carr ? C)
+ (ext_prop ? (substract_is_ext ? B C))
+(*---------------------------------------------------*) ⊢
+ ext_carr A R ≡ substract AA BB CC.