I'm doing inversion H on an Inductive definition that uses dependent types, and I obtain some assumptions of the form existT ... n = existT ... n' from which I want to deduce n = n' (this is done automatically when not using dependent types).
Concretely, here's what I think should hold but Coq doesn't do automatically
Lemma example3 (n n' : nat) :
@existT Set (fun x => x) nat n = @existT Set (fun x => x) nat n' -> n = n'.
Proof.
(* is that possible? *)
It seems to me like this should be true, but how do I prove it? Maybe it's not true, in which case why?
$ coqc --version mathieu-laptop
The Rocq Prover, version 9.0.0
compiled with OCaml 4.14.1
This lemma corresponds exactly to an axiom from the axiom wiki:
Yet another common equivalent [of axiom K] form is the injectivity of dependent pairs.
Axiom inj_dep_pair : forall (A : Type) (P : A -> Type) (p : A) (x y : P p), existT P p x = existT P p y -> x = y.
The rocq wiki page on the logic states that axiom K can be safely added (ie. won't introduce contradictions)
There are a few typical useful axioms that are independent from the Calculus of Inductive Constructions and that can be safely added to Coq [...]
Unicity of equality proofs (or equivalently Streicher's axiom K):
∀ A, ∀ x y : A, ∀ p1 p2 : x = y, p1 = p2
As observed by @Naim Favier, the axiom wiki page notes that this axiom is incompatible with univalence.
Note 2: axiom K is incompatible with the univalence axiom, which itself requires equality to be stated in Type, using the option -indices-matter.
So this suggests I have to assume an extra axiom (namely axiom K) to prove this lemma.