avoid prove_plain, export_plain, simplified after_qed;
witness = term * thm, i.e. the original proposition with a protected fact
(this achieves reliable discharge and allows facts to be slightly more general/normalized);
internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly;
ObjectLogic.ensure_propT;