matita/matita/tests/reduction_new.ma

   1 include "reduction_new_preamble.ma".
   2
   3 ndefinition test:
   4  〈〈x0,x0〉:〈x0,xF〉〉 =
   5     ((succ_w16(succ_w16(succ_w16
   6     (succ_w16(succ_w16(succ_w16(succ_w16
   7     (succ_w16(succ_w16(succ_w16(succ_w16
   8     (succ_w16(succ_w16(succ_w16(succ_w16
   9      〈〈x0,x0〉:〈x0,x0〉〉)))))))))))))))).
  10 napply (refl_eq word16 〈〈x0,x0〉:〈x0,xF〉〉);
  11 nqed.