unification hint 0 ≔ ;
x ≟ axs
(* -------------- *) ⊢
- S x ≡ A.
+ S (uax x) ≡ A. (* XXX: bug coercions/ disamb multipasso che ne fa 1 solo*)
ntheorem col2_4 :
∀A:uAx.∀a:uax A. a ◃ ∅ → ¬ a ∈ 𝐂 a one.
##]
nqed.
-ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
+(* bug interpretazione non aggiunta per ∅ *)
+ndefinition Z : Ω^axs ≝ { x | x ◃ (emptyset ?) }.
ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
#A; #a; #U; #V; #HUV; #H; nelim H; /3/;
unification hint 0 ≔ ;
x ≟ caxs
(* -------------- *) ⊢
- S x ≡ nat.
+ S (uax x) ≡ nat.
naxiom h : nat → nat.