79630933

Date: 2025-05-20 17:53:42
Score: 0.5
Natty:
Report link

Yes, it is provable in Rocq :

From Stdlib Require Export Eqdep.

Lemma example3 (n n' : nat) :
  @existT Set (fun x => x) nat n = @existT Set (fun x => x) nat n' -> n = n'.
Proof.
apply inj_pair2.
Qed.
Reasons:
  • Low length (0.5):
  • Has code block (-0.5):
  • Low reputation (0.5):
Posted by: Dave