Reductions

registration
  let p be Element of F_Real;
  reduce p + 0.F_Real to p;
  reducibility
  proof
    thus p + 0.F_Real = p;
  end;
end;