proposition: Lemma list_Rxx T (rT : T -> T -> Type) l : (forall x, rT x x) -> list_R rT l l.
proof: Proof. move=> Hr; elim: l=> [|h t IH]; [exact: list_R_nil_R|]. exact: list_R_cons_R. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) Param(Param) ProofIrrelevance