Function eq_refl_expr

crates/kernel/src/testing.rs:223–225

Convenience: Eq.refl.{u} α a

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

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

// ---- Test runner helpers ----