+
+(* Forward lemmas with t_bound rt_transition for terms **********************)
+
+lemma cnv_fwd_cpm_SO (a) (h) (G) (L):
+ ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ∃U. ⦃G,L⦄ ⊢ T ➡[1,h] U.
+#a #h #G #L #T #H
+elim (cnv_fwd_aaa … H) -H #A #HA
+/2 width=2 by aaa_cpm_SO/
+qed-.