-ninductive one : Type[0] ≝ unit : one.
-
-ndefinition force ≝
- λS:Type[2].λs:S.λT:Type[2].λt:T.λlock:one.
- match lock return λ_.Type[2] with [ unit ⇒ T].
-
-nlet rec lift (S:Type[2]) (s:S) (T:Type[2]) (t:T) (lock:one) on lock : force S s T t lock ≝
- match lock return λlock.force S s T t lock with [ unit ⇒ t ].
-
-ncoercion lift1 : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-ncoercion lift2 : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-unification hint 0 ≔ R : setoid;
- TR ≟ setoid, MR ≟ (carr R), lock ≟ unit
-(* ---------------------------------------- *) ⊢
- setoid ≡ force ?(*Type[0]*) MR TR R lock.
-
-unification hint 0 ≔ R : setoid1;
- TR ≟ setoid1, MR ≟ (carr1 R), lock ≟ unit
-(* ---------------------------------------- *) ⊢
- setoid1 ≡ force ? MR TR R lock.