(def-language indicators-language
    (embedded-language the-kernel-language)
    (base-types uu))

(def-theory indicators 
    (language indicators-language))
    

(def-language index-language
    (embedded-language indicators-language)
    (base-types index))

(def-theory family-indicators 
    (language index-language)
    (component-theories indicators))

(def-quasi-constructor predicate-to-indicator 
    "lambda(s:[uu,prop], lambda(x:uu, if(s(x), an%individual, ?unit%sort)))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor sort-to-indicator 
    "lambda(e:uu, lambda(x:uu, an%individual))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-in 
    "lambda(x:uu,a:sets[uu], #(a(x)))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-subseteq 
    "lambda(a,b:sets[uu], forall(x:uu, (x in a) implies (x in b)))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-subset 
    "lambda(a,b:sets[uu], (a subseteq b) and not(a = b))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-empty-indicator 
    "lambda(e:uu, lambda(x:uu,?unit%sort))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-nonempty-indicator? 
    "lambda(a:sets[uu], forsome(x:uu, x in a))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-empty-indicator? 
    "lambda(a:sets[uu], forall(x:uu, not(x in a)))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-complement 
    "lambda(s:sets[uu], indic(x:uu, (not #(s(x)))))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-union 
    "lambda(s,t:sets[uu], indic(x:uu, #(s(x)) or #(t(x))))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-intersection 
    "lambda(s,t:sets[uu], indic(x:uu, #(s(x)) and #(t(x))))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-difference 
    "lambda(s,t:sets[uu], indic(x:uu, #(s(x)) and (not #(t(x)))))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-sym-difference 
    "lambda(s,t:sets[uu],
            indic(x:uu, (#(s(x)) and (not #(t(x)))) or ((not #(s(x))) and #(t(x)))))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-disjoint 
    "lambda(s,t:sets[uu], forall(x:uu, not(x in s) or not(x in t)))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-partition? 
    "lambda(w:sets[sets[uu]],s:sets[uu],
          forall(u,v:sets[uu], 
              ((not (u = v)) and (u in w) and (v in w)) implies (u disj v)) and 
          forall(x:uu, (x in s) iff forsome(u:sets[uu], (u in w) and (x in u))))"
    (language indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-singleton 
    "lambda(a:uu, indic(x:uu, x=a))"
    (language indicators)
    (fixed-theories the-kernel-theory))
    

(def-quasi-constructor i-big-union 
    "lambda(f:[index,sets[uu]], indic(x:uu, forsome(i:index, #(f(i)(x)))))"
    (language family-indicators)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor i-big-intersection 
    "lambda(f:[index,sets[uu]], indic(x:uu, forall(i:index, #(f(i)(x)))))"
    (language family-indicators)
    (fixed-theories the-kernel-theory))

(def-theorem value-of-a-defined-indicator-application 
    "forall(a:sets[uu],x:uu, (x in a) implies a(x) = an%individual)"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify)))

(def-theorem meaning-of-indic-from-pred-element 
    "forall(x:uu,p:[uu,prop], (x in pred_to_indic(p)) iff p(x))"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify)))

(def-theorem meaning-of-indic-from-sort-element 
    "forall(x:uu, (x in sort_to_indic(uu)) iff #(x,uu))"
    (theory indicators)
    (usages transportable-macete)
    (proof (simplify-insistently)))