proposition: Lemma mkapp (S1 S2 T1 T2 : Type) (OP : S1 -> S2) (I1 : S1 -> T1) (I2 : S2 -> T2) (TUOP : T1 -> T2) (TUOPINJ : forall n, I2 (OP n) = TUOP (I1 n)) (s1: S1) (t1: T1) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1.
proof: Proof. subst. apply TUOPINJ. Qed.