let matinsert_lem0 = prove_by_refinement(
  `!S. (!x. P x) ==> (!x. S x ==> P x)`,
(* {{{ Proof *)
  [MESON_TAC[]]);;
(* }}} *)