The basic encoding principles are following the syntactic categories of the object-logical represent by an inductive set, The judgements of the logic are rendered as predicates over these sets, and the rules and axioms are encoded as constructors for these predicates.