proposition: Lemma mkrel (S T : Type) (R : S -> S -> Prop) (I : S -> T) (TR : T -> T -> Prop) (TRINJ : forall n m : S, R n m <-> TR (I n) (I m)) (s1 : S) (t1 : T) (P1 : I s1 = t1) (s2 : S) (t2 : T) (P2 : I s2 = t2): R s1 s2 <-> TR t1 t2.
proof: Proof. subst. apply TRINJ. Qed.