Yes, this is part of the semantics of Qed.

Thanks, I didn't know the behavior of Defined is different from Qed's. It works after I changed Qed to Defined.

BTW, if Qed is used to close the proofs, compute does nothing.

I believe the solutions contributed by others should still work in 8.11. If you don't use axioms and you close your proofs with Defined rather than Qed, the proof you give of trans_12 should work fine. You can inspect what's blocking reflexivity by first running compute after destruct; what do you see if you do that?

I'd recommend using a professional font designed for programming in that case.