Function mk_eq 

pub fn mk_eq(alpha: Expr, a: Expr, b: Expr) -> Expr

Build Eq α a b: the propositional equality type.