Function encode_bounded_expr 

pub fn encode_bounded_expr(expr: &BoundedExpr) -> Term

Encode a BoundedExpr as a kernel Term.

The encoding follows Curry-Howard:

• Bool(true) → Global(“True”) (trivially inhabited proposition)
• Bool(false) → Global(“False”) (uninhabited proposition)
• And(l, r) → App(App(Global(“And”), l’), r’)
• Or(l, r) → App(App(Global(“Or”), l’), r’)
• Not(e) → App(Global(“Not”), e’)
• Implies(l, r) → Pi(“_”, l’, r’) (function type = implication)
• Eq(l, r) → App(App(App(Global(“Eq”), Hole), l’), r’)
• Var(“sig@t”) → App(Global(“sig”), nat_literal(t))
• Int(n) → Lit(Int(n))