proposition: Lemma mkapp2 (S1 S2 S3 T1 T2 T3 : Type) (Op : S1 -> S2 -> S3) (I1 : S1 -> T1) (I2 : S2 -> T2) (I3 : S3 -> T3) (TBOP : T1 -> T2 -> T3) (TBOPINJ : forall n m, I3 (Op n m) = TBOP (I1 n) (I2 m)) (s1 : S1) (t1 : T1) (P1: I1 s1 = t1) (s2 : S2) (t2 : T2) (P2: I2 s2 = t2): I3 (Op s1 s2) = TBOP t1 t2.
proof: Proof. subst. apply TBOPINJ. Qed.