Ad
  • Custom User Avatar

    Yes, this is part of the semantics of Qed.

  • Custom User Avatar

    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?