lemma l: true.
proof -strict.
idtac.
smt.
qed.