matitaB/matita/tests/reduction_old.ma

   1 include "reduction_old_preamble.ma".
   2 definition test:
   3   〈〈x0,x0〉:〈x0,xF〉〉 =
   4     ((succ_w16(succ_w16(succ_w16
   5     (succ_w16(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      〈〈x0,x0〉:〈x0,x0〉〉)))))))))))))))).
   9 apply (refl_eq word16 〈〈x0,x0〉:〈x0,xF〉〉);
  10 qed.