#h #a #G #L #T #U1 #H #U2 #HU12
/4 width=4 by nta_conv_cnv, nta_fwd_cnv_dx, cnv_cpms_trans, cpcs_cprs_dx/
qed-.
(* Basic_1: uses: ty3_sred_back *)
lemma cprs_nta_trans (h) (a) (G) (L):
#h #a #G #L #T #U1 #H #U2 #HU12
/4 width=4 by nta_conv_cnv, nta_fwd_cnv_dx, cnv_cpms_trans, cpcs_cprs_dx/
qed-.
(* Basic_1: uses: ty3_sred_back *)
lemma cprs_nta_trans (h) (a) (G) (L):