Function eq_expr

crates/kernel/src/testing.rs:218–220

Convenience: Eq.{u} α a b

(u: MU, alpha: ME, a: ME, b: ME)

/// Convenience: Eq.{u} α a b
pub fn eq_expr(u: MU, alpha: ME, a: ME, b: ME) -> ME {
  apps(cnst("Eq", &[u]), &[alpha, a, b])
}

/// Convenience: Eq.refl.{u} α a
pub fn eq_refl_expr(u: MU, alpha: ME, a: ME) -> ME {