If you want to show such equality, you need to (1) show that the main functions are equal (i.e., the R components of your sigma type) and (2) show that the corresponding proofs are equal, however, there are two problems.
The first is that the equality of functions is too weak in Coq. According to general mathematical practice, we expect two functions to be equal if they bring equal results for any input. This principle is known as functional extensibility:
Axiom functional_extensionality : forall A (B : A -> Type) (fg : forall a, B a), (forall x, fx = gx) -> f = g.
Oddly enough, this principle is not proved in the logic of Coq! Roughly speaking, the only way two functions can be equal is that they can be converted to syntactically equal members in accordance with the rules for computing logic. For example, we can show that fun n : nat => 0 + n and fun n : nat => n are equal, because + is defined in Coq by matching patterns by the first argument, and the first argument in the first member is 0 .
Goal (fun n : nat => 0 + n) = (fun n : nat => n). reflexivity. Qed.
We could expect to show that fun n => n + 0 and fun n => n are equal in a similar way. However, Coq does not accept this because + cannot be simplified when the first argument is a variable.
Another problem is that the concept of equality on evidence is also not very interesting. The only way to show that the two proofs are equal is again syntactic equality. Intuitively, however, I would like to argue with the proof of inconsistency, a principle that claims that evidence of the same is always always equal:
Axiom proof_irrelevance : forall (P : Prop) (pq : P), p = q.
but, again, this principle is not proved in logic. Fortunately, the Coq logic has been designed so that these principles can be added as axioms. Then we get the following proof:
Axiom functional_extensionality : forall A (B : A -> Type) (fg : forall a, B a), (forall a, fa = ga) -> f = g. Axiom proof_irrelevance : forall (P : Prop) (pq : P), p = q. Lemma l (r1 r2 : { R : nat -> nat -> bool | forall n, R nn = true }) : (forall n1 n2, proj1_sig r1 n1 n2 = proj1_sig r2 n1 n2) -> r1 = r2. Proof. destruct r1 as [r1 H1], r2 as [r2 H2]. simpl. intros H. assert (H' : r1 = r2). { apply functional_extensionality. intros n1. apply functional_extensionality. intros n2. apply H. } subst r2. rename r1 into r. f_equal. apply proof_irrelevance. Qed.
Even if axioms can be useful, they could be avoided. In this case, in fact, this lemma can be proved only with functional extensibility, but you need it at least. If you want to avoid using axioms, and r1 and r2 not equal before calculation, you will have to use the equivalence equivalence relation for your type, and instead do your formalization using this relation, for example
Definition rel_equiv (r1 r2 : { R : nat -> nat -> bool | forall n, R nn = true }) : Prop := forall n1 n2, proj1_sig r1 n1 n2 = proj2_sig r2 n1 n2.
The standard library has good support for rewriting with equivalence relations; Wed for example this .