(def-translation the-kernel-translation 
    (source the-kernel-theory)
    (target the-kernel-theory))

(def-language pure-generic-language-1
    (base-types ind_1))

(def-language pure-generic-language-2
    (embedded-language pure-generic-language-1)
    (base-types ind_2))

(def-language pure-generic-language-3
    (embedded-language pure-generic-language-2)
    (base-types ind_3))

(def-language pure-generic-language-4
    (embedded-language pure-generic-language-3)
    (base-types ind_4))

(def-theory pure-generic-theory-0) 

(def-theory pure-generic-theory-1 
    (language pure-generic-language-1)
    (component-theories pure-generic-theory-0))

(def-theory pure-generic-theory-2 
    (language pure-generic-language-2)
    (component-theories pure-generic-theory-1))

(def-theory pure-generic-theory-3 
    (language pure-generic-language-3)
    (component-theories pure-generic-theory-2))

(def-theory pure-generic-theory-4 
    (language pure-generic-language-4)
    (component-theories pure-generic-theory-3))

(def-theorem definedness-of-dangling-conditionals 
    "forall(a:prop,b:ind_1, #(if(a,b,?ind_1)) iff a)"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof (simplify)))